theorem :: NDIFF11:17

for n being non zero Nat
for i being Nat
for x being Point of (REAL-NS n) st 1 <= i & i <= n holds
( Proj (i,n) is_differentiable_in x & diff ((Proj (i,n)),x) = Proj (i,n) )