let n, m be non zero Nat; :: thesis: for i being Nat
for g being PartFunc of (REAL m),(REAL n)
for y being Element of REAL m st g is_differentiable_in y & 1 <= i & i <= m holds
( g is_partial_differentiable_in y,i & partdiff (g,y,i) = ((diff (g,y)) * (reproj (i,(0. (REAL-NS m))))) . <*1*> )
let i be Nat; :: thesis: for g being PartFunc of (REAL m),(REAL n)
for y being Element of REAL m st g is_differentiable_in y & 1 <= i & i <= m holds
( g is_partial_differentiable_in y,i & partdiff (g,y,i) = ((diff (g,y)) * (reproj (i,(0. (REAL-NS m))))) . <*1*> )
let g be PartFunc of (REAL m),(REAL n); :: thesis: for y being Element of REAL m st g is_differentiable_in y & 1 <= i & i <= m holds
( g is_partial_differentiable_in y,i & partdiff (g,y,i) = ((diff (g,y)) * (reproj (i,(0. (REAL-NS m))))) . <*1*> )
let y be Element of REAL m; :: thesis: ( g is_differentiable_in y & 1 <= i & i <= m implies ( g is_partial_differentiable_in y,i & partdiff (g,y,i) = ((diff (g,y)) * (reproj (i,(0. (REAL-NS m))))) . <*1*> ) )
assume A1: ( g is_differentiable_in y & 1 <= i & i <= m ) ; :: thesis: ( g is_partial_differentiable_in y,i & partdiff (g,y,i) = ((diff (g,y)) * (reproj (i,(0. (REAL-NS m))))) . <*1*> )
then consider f being PartFunc of (REAL-NS m),(REAL-NS n), x being Point of (REAL-NS m) such that
A2: ( f = g & x = y & f is_differentiable_in x ) ;
A3: ex f2 being PartFunc of (REAL-NS m),(REAL-NS n) ex x2 being Point of (REAL-NS m) st
( f2 = g & x2 = y & diff (g,y) = diff (f2,x2) ) by A1, PDIFF_1:def 8;
A4: ( f is_partial_differentiable_in x,i & partdiff (f,x,i) = (diff (f,x)) * (reproj (i,(0. (REAL-NS m)))) ) by Th21, A2, A1;
then g is_partial_differentiable_in y,i by A2;
then ex f1 being PartFunc of (REAL-NS m),(REAL-NS n) ex x1 being Point of (REAL-NS m) st
( f1 = g & x1 = y & partdiff (g,y,i) = (partdiff (f1,x1,i)) . <*1*> ) by PDIFF_1:def 14;
hence ( g is_partial_differentiable_in y,i & partdiff (g,y,i) = ((diff (g,y)) * (reproj (i,(0. (REAL-NS m))))) . <*1*> ) by A4, A3, A2; :: thesis: verum