let m be non zero Nat; 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; 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; 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; ( 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 )
; ( 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; ( 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))
; 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; verum