let n be non empty Element of NAT ; :: thesis: for i being Element of NAT
for g being PartFunc of REAL n, REAL
for y being Element of REAL n
for g1 being PartFunc of REAL n, REAL 1 st g1 = <>* g & g1 is_partial_differentiable_in y,i holds
partdiff g1,y,i = <*(partdiff g,y,i)*>
let i be Element of NAT ; :: thesis: for g being PartFunc of REAL n, REAL
for y being Element of REAL n
for g1 being PartFunc of REAL n, REAL 1 st g1 = <>* g & g1 is_partial_differentiable_in y,i holds
partdiff g1,y,i = <*(partdiff g,y,i)*>
let g be PartFunc of REAL n, REAL ; :: thesis: for y being Element of REAL n
for g1 being PartFunc of REAL n, REAL 1 st g1 = <>* g & g1 is_partial_differentiable_in y,i holds
partdiff g1,y,i = <*(partdiff g,y,i)*>
let y be Element of REAL n; :: thesis: for g1 being PartFunc of REAL n, REAL 1 st g1 = <>* g & g1 is_partial_differentiable_in y,i holds
partdiff g1,y,i = <*(partdiff g,y,i)*>
let g1 be PartFunc of REAL n, REAL 1; :: thesis: ( g1 = <>* g & g1 is_partial_differentiable_in y,i implies partdiff g1,y,i = <*(partdiff g,y,i)*> )
assume A1: ( g1 = <>* g & g1 is_partial_differentiable_in y,i ) ; :: thesis: partdiff g1,y,i = <*(partdiff g,y,i)*>
( the carrier of (REAL-NS 1) = REAL 1 & the carrier of (REAL-NS n) = REAL n ) by REAL_NS1:def 4;
then reconsider h = g1 as PartFunc of (REAL-NS n),(REAL-NS 1) ;
reconsider y' = y as Point of (REAL-NS n) by REAL_NS1:def 4;
A2: h is_partial_differentiable_in y',i by A1, Th16;
then (partdiff h,y',i) . <*1*> = partdiff g1,y,i by Th17;
hence partdiff g1,y,i = <*(partdiff g,y,i)*> by A1, A2, Th15; :: thesis: verum