let m be non empty Element of NAT ; :: thesis: for i being Element of 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 Element of 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) )
then <>* h is_differentiable_in y by Def1;
then 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 ) by PDIFF_1:def 13;
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 PDIFF_1:def 14, A2;
<*1*> in REAL 1 by FINSEQ_2:118;
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, FUNCT_2:21, A5;
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 PDIFF_1:def 6, A5;
then (reproj i,(0. (REAL-NS m))) . <*1*> = (reproj i,(0* m)) . 1 by FINSEQ_1:97;
then partdiff h,y,i = (proj 1,1) . ((diff (<>* h),y) . ((reproj i,(0* m)) . 1)) by A6, PDIFF_1:1;
hence partdiff h,y,i = (diff h,y) . ((reproj i,(0* m)) . 1) by FUNCT_2:21; :: thesis: verum