let n, m be non empty Element of NAT ; :: thesis: for i being Element of 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 Element of 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 ) by PDIFF_1:def 7;
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, PDIFF_1:def 13;
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, PDIFF_1:def 13; :: thesis: verum