For differentiable maps at and at , the chain rule asserts
Write with , and with . Since , substitution gives
Both remaining terms are , proving differentiability and the stated chain rule. The estimate for also holds when its argument is zero, by setting .
For the circle constraint take . The composite is constant, so the chain rule gives
Since , this is a nonzero row vector annihilating . Thus cannot be invertible: at every . Geometrically, the derivative of a map into a level set takes values in the tangent space to the circle.