let n be non zero Nat; :: thesis: for i being Nat

for g1, g2 being PartFunc of (REAL n),REAL

for y being Element of REAL n st g1 is_partial_differentiable_in y,i & g2 is_partial_differentiable_in y,i holds

( g1 + g2 is_partial_differentiable_in y,i & partdiff ((g1 + g2),y,i) = (partdiff (g1,y,i)) + (partdiff (g2,y,i)) )

let i be Nat; :: thesis: for g1, g2 being PartFunc of (REAL n),REAL

for y being Element of REAL n st g1 is_partial_differentiable_in y,i & g2 is_partial_differentiable_in y,i holds

( g1 + g2 is_partial_differentiable_in y,i & partdiff ((g1 + g2),y,i) = (partdiff (g1,y,i)) + (partdiff (g2,y,i)) )

let g1, g2 be PartFunc of (REAL n),REAL; :: thesis: for y being Element of REAL n st g1 is_partial_differentiable_in y,i & g2 is_partial_differentiable_in y,i holds

( g1 + g2 is_partial_differentiable_in y,i & partdiff ((g1 + g2),y,i) = (partdiff (g1,y,i)) + (partdiff (g2,y,i)) )

let y be Element of REAL n; :: thesis: ( g1 is_partial_differentiable_in y,i & g2 is_partial_differentiable_in y,i implies ( g1 + g2 is_partial_differentiable_in y,i & partdiff ((g1 + g2),y,i) = (partdiff (g1,y,i)) + (partdiff (g2,y,i)) ) )

assume that

A1: g1 is_partial_differentiable_in y,i and

A2: g2 is_partial_differentiable_in y,i ; :: thesis: ( g1 + g2 is_partial_differentiable_in y,i & partdiff ((g1 + g2),y,i) = (partdiff (g1,y,i)) + (partdiff (g2,y,i)) )

reconsider x = y as Point of (REAL-NS n) by REAL_NS1:def 4;

A3: the carrier of (REAL-NS 1) = REAL 1 by REAL_NS1:def 4;

then reconsider f1 = <>* g1, f2 = <>* g2 as PartFunc of (REAL-NS n),(REAL-NS 1) by REAL_NS1:def 4;

reconsider One = <*jj*> as VECTOR of (REAL-NS 1) by A3, FINSEQ_2:98;

A4: f1 is_partial_differentiable_in x,i by A1, Th14;

then A5: (partdiff (f1,x,i)) . One = <*(partdiff (g1,y,i))*> by Th15;

reconsider d2 = partdiff (g2,y,i) as Element of REAL by XREAL_0:def 1;

reconsider Pd2 = <*d2*> as Element of REAL 1 by FINSEQ_2:98;

reconsider d1 = partdiff (g1,y,i) as Element of REAL by XREAL_0:def 1;

reconsider Pd1 = <*d1*> as Element of REAL 1 by FINSEQ_2:98;

A6: the carrier of (REAL-NS n) = REAL n by REAL_NS1:def 4;

rng g2 c= dom ((proj (1,1)) ") by Th2;

then A7: dom (((proj (1,1)) ") * g2) = dom g2 by RELAT_1:27;

rng g1 c= dom ((proj (1,1)) ") by Th2;

then A8: dom (((proj (1,1)) ") * g1) = dom g1 by RELAT_1:27;

then dom (f1 + f2) = (dom g1) /\ (dom g2) by A7, VFUNCT_1:def 1;

then A9: dom (f1 + f2) = dom (g1 + g2) by VALUED_1:def 1;

A10: rng (g1 + g2) c= dom ((proj (1,1)) ") by Th2;

then A11: dom (((proj (1,1)) ") * (g1 + g2)) = dom (g1 + g2) by RELAT_1:27;

then A21: (partdiff (f2,x,i)) . One = <*(partdiff (g2,y,i))*> by Th15;

A22: f1 + f2 is_partial_differentiable_in x,i by A4, A20, Th28;

dom (f1 + f2) = dom (<>* (g1 + g2)) by A9, A10, RELAT_1:27;

then A23: f1 + f2 = <>* (g1 + g2) by A6, A3, A12, PARTFUN1:5;

then <*(partdiff ((g1 + g2),y,i))*> = (partdiff ((f1 + f2),x,i)) . <*1*> by A4, A20, Th15, Th28

.= ((partdiff (f1,x,i)) + (partdiff (f2,x,i))) . <*1*> by A4, A20, Th28

.= ((partdiff (f1,x,i)) . One) + ((partdiff (f2,x,i)) . One) by LOPBAN_1:35

.= Pd1 + Pd2 by A5, A21, REAL_NS1:2

.= <*((partdiff (g1,y,i)) + (partdiff (g2,y,i)))*> by RVSUM_1:13 ;

then partdiff ((g1 + g2),y,i) = <*((partdiff (g1,y,i)) + (partdiff (g2,y,i)))*> . 1 by FINSEQ_1:40;

hence ( g1 + g2 is_partial_differentiable_in y,i & partdiff ((g1 + g2),y,i) = (partdiff (g1,y,i)) + (partdiff (g2,y,i)) ) by A23, A22, Th14, FINSEQ_1:40; :: thesis: verum

for g1, g2 being PartFunc of (REAL n),REAL

for y being Element of REAL n st g1 is_partial_differentiable_in y,i & g2 is_partial_differentiable_in y,i holds

( g1 + g2 is_partial_differentiable_in y,i & partdiff ((g1 + g2),y,i) = (partdiff (g1,y,i)) + (partdiff (g2,y,i)) )

let i be Nat; :: thesis: for g1, g2 being PartFunc of (REAL n),REAL

for y being Element of REAL n st g1 is_partial_differentiable_in y,i & g2 is_partial_differentiable_in y,i holds

( g1 + g2 is_partial_differentiable_in y,i & partdiff ((g1 + g2),y,i) = (partdiff (g1,y,i)) + (partdiff (g2,y,i)) )

let g1, g2 be PartFunc of (REAL n),REAL; :: thesis: for y being Element of REAL n st g1 is_partial_differentiable_in y,i & g2 is_partial_differentiable_in y,i holds

( g1 + g2 is_partial_differentiable_in y,i & partdiff ((g1 + g2),y,i) = (partdiff (g1,y,i)) + (partdiff (g2,y,i)) )

let y be Element of REAL n; :: thesis: ( g1 is_partial_differentiable_in y,i & g2 is_partial_differentiable_in y,i implies ( g1 + g2 is_partial_differentiable_in y,i & partdiff ((g1 + g2),y,i) = (partdiff (g1,y,i)) + (partdiff (g2,y,i)) ) )

assume that

A1: g1 is_partial_differentiable_in y,i and

A2: g2 is_partial_differentiable_in y,i ; :: thesis: ( g1 + g2 is_partial_differentiable_in y,i & partdiff ((g1 + g2),y,i) = (partdiff (g1,y,i)) + (partdiff (g2,y,i)) )

reconsider x = y as Point of (REAL-NS n) by REAL_NS1:def 4;

A3: the carrier of (REAL-NS 1) = REAL 1 by REAL_NS1:def 4;

then reconsider f1 = <>* g1, f2 = <>* g2 as PartFunc of (REAL-NS n),(REAL-NS 1) by REAL_NS1:def 4;

reconsider One = <*jj*> as VECTOR of (REAL-NS 1) by A3, FINSEQ_2:98;

A4: f1 is_partial_differentiable_in x,i by A1, Th14;

then A5: (partdiff (f1,x,i)) . One = <*(partdiff (g1,y,i))*> by Th15;

reconsider d2 = partdiff (g2,y,i) as Element of REAL by XREAL_0:def 1;

reconsider Pd2 = <*d2*> as Element of REAL 1 by FINSEQ_2:98;

reconsider d1 = partdiff (g1,y,i) as Element of REAL by XREAL_0:def 1;

reconsider Pd1 = <*d1*> as Element of REAL 1 by FINSEQ_2:98;

A6: the carrier of (REAL-NS n) = REAL n by REAL_NS1:def 4;

rng g2 c= dom ((proj (1,1)) ") by Th2;

then A7: dom (((proj (1,1)) ") * g2) = dom g2 by RELAT_1:27;

rng g1 c= dom ((proj (1,1)) ") by Th2;

then A8: dom (((proj (1,1)) ") * g1) = dom g1 by RELAT_1:27;

then dom (f1 + f2) = (dom g1) /\ (dom g2) by A7, VFUNCT_1:def 1;

then A9: dom (f1 + f2) = dom (g1 + g2) by VALUED_1:def 1;

A10: rng (g1 + g2) c= dom ((proj (1,1)) ") by Th2;

then A11: dom (((proj (1,1)) ") * (g1 + g2)) = dom (g1 + g2) by RELAT_1:27;

A12: now :: thesis: for x being Element of (REAL-NS n) st x in dom (f1 + f2) holds

(f1 + f2) . x = (<>* (g1 + g2)) . x

A20:
f2 is_partial_differentiable_in x,i
by A2, Th14;(f1 + f2) . x = (<>* (g1 + g2)) . x

let x be Element of (REAL-NS n); :: thesis: ( x in dom (f1 + f2) implies (f1 + f2) . x = (<>* (g1 + g2)) . x )

assume A13: x in dom (f1 + f2) ; :: thesis: (f1 + f2) . x = (<>* (g1 + g2)) . x

then (f1 + f2) . x = (f1 + f2) /. x by PARTFUN1:def 6;

then A14: (f1 + f2) . x = (f1 /. x) + (f2 /. x) by A13, VFUNCT_1:def 1;

A15: x in (dom f1) /\ (dom f2) by A13, VFUNCT_1:def 1;

then x in dom f1 by XBOOLE_0:def 4;

then A16: f1 /. x = (((proj (1,1)) ") * g1) . x by PARTFUN1:def 6;

x in dom f2 by A15, XBOOLE_0:def 4;

then A17: f2 /. x = (((proj (1,1)) ") * g2) . x by PARTFUN1:def 6;

x in dom g2 by A7, A15, XBOOLE_0:def 4;

then A18: f2 /. x = ((proj (1,1)) ") . (g2 . x) by A17, FUNCT_1:13;

x in dom g1 by A8, A15, XBOOLE_0:def 4;

then A19: f1 /. x = ((proj (1,1)) ") . (g1 . x) by A16, FUNCT_1:13;

(<>* (g1 + g2)) . x = ((proj (1,1)) ") . ((g1 + g2) . x) by A9, A11, A13, FUNCT_1:12;

then (<>* (g1 + g2)) . x = ((proj (1,1)) ") . ((g1 . x) + (g2 . x)) by A9, A13, VALUED_1:def 1;

hence (f1 + f2) . x = (<>* (g1 + g2)) . x by A14, A19, A18, Th2, Th3; :: thesis: verum

end;assume A13: x in dom (f1 + f2) ; :: thesis: (f1 + f2) . x = (<>* (g1 + g2)) . x

then (f1 + f2) . x = (f1 + f2) /. x by PARTFUN1:def 6;

then A14: (f1 + f2) . x = (f1 /. x) + (f2 /. x) by A13, VFUNCT_1:def 1;

A15: x in (dom f1) /\ (dom f2) by A13, VFUNCT_1:def 1;

then x in dom f1 by XBOOLE_0:def 4;

then A16: f1 /. x = (((proj (1,1)) ") * g1) . x by PARTFUN1:def 6;

x in dom f2 by A15, XBOOLE_0:def 4;

then A17: f2 /. x = (((proj (1,1)) ") * g2) . x by PARTFUN1:def 6;

x in dom g2 by A7, A15, XBOOLE_0:def 4;

then A18: f2 /. x = ((proj (1,1)) ") . (g2 . x) by A17, FUNCT_1:13;

x in dom g1 by A8, A15, XBOOLE_0:def 4;

then A19: f1 /. x = ((proj (1,1)) ") . (g1 . x) by A16, FUNCT_1:13;

(<>* (g1 + g2)) . x = ((proj (1,1)) ") . ((g1 + g2) . x) by A9, A11, A13, FUNCT_1:12;

then (<>* (g1 + g2)) . x = ((proj (1,1)) ") . ((g1 . x) + (g2 . x)) by A9, A13, VALUED_1:def 1;

hence (f1 + f2) . x = (<>* (g1 + g2)) . x by A14, A19, A18, Th2, Th3; :: thesis: verum

then A21: (partdiff (f2,x,i)) . One = <*(partdiff (g2,y,i))*> by Th15;

A22: f1 + f2 is_partial_differentiable_in x,i by A4, A20, Th28;

dom (f1 + f2) = dom (<>* (g1 + g2)) by A9, A10, RELAT_1:27;

then A23: f1 + f2 = <>* (g1 + g2) by A6, A3, A12, PARTFUN1:5;

then <*(partdiff ((g1 + g2),y,i))*> = (partdiff ((f1 + f2),x,i)) . <*1*> by A4, A20, Th15, Th28

.= ((partdiff (f1,x,i)) + (partdiff (f2,x,i))) . <*1*> by A4, A20, Th28

.= ((partdiff (f1,x,i)) . One) + ((partdiff (f2,x,i)) . One) by LOPBAN_1:35

.= Pd1 + Pd2 by A5, A21, REAL_NS1:2

.= <*((partdiff (g1,y,i)) + (partdiff (g2,y,i)))*> by RVSUM_1:13 ;

then partdiff ((g1 + g2),y,i) = <*((partdiff (g1,y,i)) + (partdiff (g2,y,i)))*> . 1 by FINSEQ_1:40;

hence ( g1 + g2 is_partial_differentiable_in y,i & partdiff ((g1 + g2),y,i) = (partdiff (g1,y,i)) + (partdiff (g2,y,i)) ) by A23, A22, Th14, FINSEQ_1:40; :: thesis: verum