let i be Element of NAT ; :: thesis: for n being non zero Element of NAT
for f being PartFunc of REAL,(REAL n)
for x0 being Real st 1 <= i & i <= n & f is_differentiable_in x0 holds
( (Proj (i,n)) * f is_differentiable_in x0 & (Proj (i,n)) . (diff (f,x0)) = diff (((Proj (i,n)) * f),x0) )
let n be non zero Element of NAT ; :: thesis: for f being PartFunc of REAL,(REAL n)
for x0 being Real st 1 <= i & i <= n & f is_differentiable_in x0 holds
( (Proj (i,n)) * f is_differentiable_in x0 & (Proj (i,n)) . (diff (f,x0)) = diff (((Proj (i,n)) * f),x0) )
let f be PartFunc of REAL,(REAL n); :: thesis: for x0 being Real st 1 <= i & i <= n & f is_differentiable_in x0 holds
( (Proj (i,n)) * f is_differentiable_in x0 & (Proj (i,n)) . (diff (f,x0)) = diff (((Proj (i,n)) * f),x0) )
let x0 be Real; :: thesis: ( 1 <= i & i <= n & f is_differentiable_in x0 implies ( (Proj (i,n)) * f is_differentiable_in x0 & (Proj (i,n)) . (diff (f,x0)) = diff (((Proj (i,n)) * f),x0) ) )
assume A1: ( 1 <= i & i <= n & f is_differentiable_in x0 ) ; :: thesis: ( (Proj (i,n)) * f is_differentiable_in x0 & (Proj (i,n)) . (diff (f,x0)) = diff (((Proj (i,n)) * f),x0) )
then consider g being PartFunc of REAL,(REAL-NS n) such that
A2: ( f = g & g is_differentiable_in x0 ) ;
diff (f,x0) = diff (g,x0) by A2, Th3;
hence ( (Proj (i,n)) * f is_differentiable_in x0 & (Proj (i,n)) . (diff (f,x0)) = diff (((Proj (i,n)) * f),x0) ) by A2, A1, Th24; :: thesis: verum