let n be non zero Nat; :: thesis: for i being 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 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;
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