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 that
A1: g1 = <>* g and
A2: g1 is_partial_differentiable_in y,i ; :: thesis: partdiff g1,y,i = <*(partdiff g,y,i)*>
reconsider y9 = y as Point of (REAL-NS n) by REAL_NS1:def 4;
the carrier of (REAL-NS 1) = REAL 1 by REAL_NS1:def 4;
then reconsider h = g1 as PartFunc of (REAL-NS n),(REAL-NS 1) by REAL_NS1:def 4;
A3: h is_partial_differentiable_in y9,i by A2, Th16;
then (partdiff h,y9,i) . <*1*> = partdiff g1,y,i by Th17;
hence partdiff g1,y,i = <*(partdiff g,y,i)*> by A1, A3, Th15; :: thesis: verum