In control engineering, differentiable partial functions from R into Rn play a very important role. In this article, we formalized basic properties of such functions.