let n be non zero Nat; :: thesis: 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) )
let i be Nat; :: thesis: 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) )
let x be Point of (REAL-NS n); :: thesis: ( 1 <= i & i <= n implies ( Proj (i,n) is_differentiable_in x & diff ((Proj (i,n)),x) = Proj (i,n) ) )
assume A1: ( 1 <= i & i <= n ) ; :: thesis: ( Proj (i,n) is_differentiable_in x & diff ((Proj (i,n)),x) = Proj (i,n) )
n is non zero Element of NAT by ORDINAL1:def 12;
then Proj (i,n) is Lipschitzian LinearOperator of (REAL-NS n),(REAL-NS 1) by A1, PDIFF_8:6;
hence ( Proj (i,n) is_differentiable_in x & diff ((Proj (i,n)),x) = Proj (i,n) ) by Th16; :: thesis: verum