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

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