A regular level set in a Banach space

Assume the Axiom of Choice (The Axiom of Choice). Let $K$ and $Y$ be real Banach spaces (Banach space) and let $X=K\oplus Y$ be their topological direct sum, with bounded coordinate projections (A complemented closed subspace of a normed space), where the direct sum is second countable (Second countability: an at most countable basis for the topology) — for instance this holds whenever $K$ and $Y$ are second countable, since the direct sum is a finite product (Assuming countable choice, a countable product of second countable spaces is second countable). Equip $X$ and $Y$ with their standard maximal $C^{\mathrm{\infty }}$ atlases, namely the maximal atlases containing their global identity charts. Then $X$ and $Y$ are $C^{\mathrm{\infty }}$ Banach manifolds in the sense of Countable base Banach manifold and smooth map, and the projection $p:X\to Y$, $p(k+y):=y$, has every $y\in Y$ as a regular value in the sense of the regular value theorem (Regular value theorem for Banach manifolds): $p$ is smooth — a bounded linear map equals its own derivative everywhere — and at every point of $p^{-1}(y)$ its derivative is onto with complemented kernel. Each level set $p^{-1}(y)$ is the affine split submanifold

$p^{-1}(y)=K+y=\{k+y:k\in K\}$

of $X$, and its tangent space at every point is $K$.