let m be non zero Nat; :: thesis: for i being Nat
for h being PartFunc of (REAL m),REAL
for y being Element of REAL m st h is_differentiable_in y & 1 <= i & i <= m holds
( h is_partial_differentiable_in y,i & partdiff (h,y,i) = diff ((h * (reproj (i,y))),((proj (i,m)) . y)) & partdiff (h,y,i) = (diff (h,y)) . ((reproj (i,(0* m))) . 1) )
let i be Nat; :: thesis: for h being PartFunc of (REAL m),REAL
for y being Element of REAL m st h is_differentiable_in y & 1 <= i & i <= m holds
( h is_partial_differentiable_in y,i & partdiff (h,y,i) = diff ((h * (reproj (i,y))),((proj (i,m)) . y)) & partdiff (h,y,i) = (diff (h,y)) . ((reproj (i,(0* m))) . 1) )
let h be PartFunc of (REAL m),REAL; :: thesis: for y being Element of REAL m st h is_differentiable_in y & 1 <= i & i <= m holds
( h is_partial_differentiable_in y,i & partdiff (h,y,i) = diff ((h * (reproj (i,y))),((proj (i,m)) . y)) & partdiff (h,y,i) = (diff (h,y)) . ((reproj (i,(0* m))) . 1) )
let y be Element of REAL m; :: thesis: ( h is_differentiable_in y & 1 <= i & i <= m implies ( h is_partial_differentiable_in y,i & partdiff (h,y,i) = diff ((h * (reproj (i,y))),((proj (i,m)) . y)) & partdiff (h,y,i) = (diff (h,y)) . ((reproj (i,(0* m))) . 1) ) )
assume A1: ( h is_differentiable_in y & 1 <= i & i <= m ) ; :: thesis: ( h is_partial_differentiable_in y,i & partdiff (h,y,i) = diff ((h * (reproj (i,y))),((proj (i,m)) . y)) & partdiff (h,y,i) = (diff (h,y)) . ((reproj (i,(0* m))) . 1) )
A2: ( <>* h is_partial_differentiable_in y,i & partdiff ((<>* h),y,i) = ((diff ((<>* h),y)) * (reproj (i,(0. (REAL-NS m))))) . <*1*> ) by Th22, A1;
then A3: ex g being PartFunc of (REAL-NS m),(REAL-NS 1) ex x being Point of (REAL-NS m) st
( <>* h = g & x = y & g is_partial_differentiable_in x,i ) ;
hence h is_partial_differentiable_in y,i by PDIFF_1:14; :: thesis: ( partdiff (h,y,i) = diff ((h * (reproj (i,y))),((proj (i,m)) . y)) & partdiff (h,y,i) = (diff (h,y)) . ((reproj (i,(0* m))) . 1) )
thus partdiff (h,y,i) = diff ((h * (reproj (i,y))),((proj (i,m)) . y)) ; :: thesis: partdiff (h,y,i) = (diff (h,y)) . ((reproj (i,(0* m))) . 1)
A4: ex k being PartFunc of (REAL-NS m),(REAL-NS 1) ex z being Point of (REAL-NS m) st
( <>* h = k & y = z & partdiff ((<>* h),y,i) = (partdiff (k,z,i)) . <*1*> ) by A2, PDIFF_1:def 14;
<*jj*> in REAL 1 by FINSEQ_2:98;
then A5: <*1*> in the carrier of (REAL-NS 1) by REAL_NS1:def 4;
<*(partdiff (h,y,i))*> = partdiff ((<>* h),y,i) by A4, A3, PDIFF_1:15;
then A6: <*(partdiff (h,y,i))*> = (diff ((<>* h),y)) . ((reproj (i,(0. (REAL-NS m)))) . <*1*>) by A2, A5, FUNCT_2:15;
0. (REAL-NS m) = 0* m by REAL_NS1:def 4;
then ex q being Element of REAL ex z being Element of REAL m st
( <*1*> = <*q*> & z = 0* m & (reproj (i,(0. (REAL-NS m)))) . <*1*> = (reproj (i,z)) . q ) by A5, PDIFF_1:def 6;
then (reproj (i,(0. (REAL-NS m)))) . <*1*> = (reproj (i,(0* m))) . 1 by FINSEQ_1:76;
then partdiff (h,y,i) = (proj (1,1)) . ((diff ((<>* h),y)) . ((reproj (i,(0* m))) . jj)) by A6, PDIFF_1:1;
hence partdiff (h,y,i) = (diff (h,y)) . ((reproj (i,(0* m))) . 1) by FUNCT_2:15; :: thesis: verum