Let , and . Fix and choose the allowed slice chart for an embedded submanifold on a neighborhood of , so that is given by . On define the smooth map
The derivative at a point of is surjective and has kernel , by the slice description. The printed sum-of-spaces condition gives
Indeed any target tangent vector is a sum of an image vector and a tangent vector to , and kills the latter. By the chain rule, is therefore surjective. This condition is precisely transversality of a map to a submanifold; the original sum need not be direct.
We have . Part (b), applied to , gives slice charts for an embedded submanifold of codimension around every point of this zero set. Since the construction is available around every , the charts give its global structure as an embedded submanifold with the subspace topology. Its dimension is . Moreover,
This follows either from the slice coordinates or from and . No injectivity of , closedness of , or direct-sum hypothesis is required.
If satisfies transversality of a map to a submanifold , its nonempty preimage is an embedded submanifold of the displayed codimension. Choose a slice chart for an embedded submanifold around in which is the zero set of the first coordinates. Their composition with has surjective derivative on its zero set, so the regular level set theorem gives a local embedded slice of dimension . These slices give the subspace topology and a compatible smooth atlas on the preimage. Its tangent space is