let x0 be Real; :: thesis: for f1, f2 being PartFunc of REAL,REAL st f1 is_differentiable_in x0 & f2 is_differentiable_in x0 holds

( f1 + f2 is_differentiable_in x0 & diff ((f1 + f2),x0) = (diff (f1,x0)) + (diff (f2,x0)) )

let f1, f2 be PartFunc of REAL,REAL; :: thesis: ( f1 is_differentiable_in x0 & f2 is_differentiable_in x0 implies ( f1 + f2 is_differentiable_in x0 & diff ((f1 + f2),x0) = (diff (f1,x0)) + (diff (f2,x0)) ) )

reconsider j = 1 as Element of REAL by XREAL_0:def 1;

assume that

A1: f1 is_differentiable_in x0 and

A2: f2 is_differentiable_in x0 ; :: thesis: ( f1 + f2 is_differentiable_in x0 & diff ((f1 + f2),x0) = (diff (f1,x0)) + (diff (f2,x0)) )

consider N1 being Neighbourhood of x0 such that

A3: N1 c= dom f1 and

A4: ex L being LinearFunc ex R being RestFunc st

for x being Real st x in N1 holds

(f1 . x) - (f1 . x0) = (L . (x - x0)) + (R . (x - x0)) by A1;

consider L1 being LinearFunc, R1 being RestFunc such that

A5: for x being Real st x in N1 holds

(f1 . x) - (f1 . x0) = (L1 . (x - x0)) + (R1 . (x - x0)) by A4;

consider N2 being Neighbourhood of x0 such that

A6: N2 c= dom f2 and

A7: ex L being LinearFunc ex R being RestFunc st

for x being Real st x in N2 holds

(f2 . x) - (f2 . x0) = (L . (x - x0)) + (R . (x - x0)) by A2;

consider L2 being LinearFunc, R2 being RestFunc such that

A8: for x being Real st x in N2 holds

(f2 . x) - (f2 . x0) = (L2 . (x - x0)) + (R2 . (x - x0)) by A7;

reconsider R = R1 + R2 as RestFunc by Th4;

reconsider L = L1 + L2 as LinearFunc by Th2;

A9: ( L1 is total & L2 is total ) by Def3;

consider N being Neighbourhood of x0 such that

A10: N c= N1 and

A11: N c= N2 by RCOMP_1:17;

A12: N c= dom f2 by A6, A11;

N c= dom f1 by A3, A10;

then N /\ N c= (dom f1) /\ (dom f2) by A12, XBOOLE_1:27;

then A13: N c= dom (f1 + f2) by VALUED_1:def 1;

A14: ( R1 is total & R2 is total ) by Def2;

hence diff ((f1 + f2),x0) = L . 1 by A13, A15, Def5

.= (L1 . j) + (L2 . j) by A9, RFUNCT_1:56

.= (diff (f1,x0)) + (L2 . 1) by A1, A3, A5, Def5

.= (diff (f1,x0)) + (diff (f2,x0)) by A2, A6, A8, Def5 ;

:: thesis: verum

( f1 + f2 is_differentiable_in x0 & diff ((f1 + f2),x0) = (diff (f1,x0)) + (diff (f2,x0)) )

let f1, f2 be PartFunc of REAL,REAL; :: thesis: ( f1 is_differentiable_in x0 & f2 is_differentiable_in x0 implies ( f1 + f2 is_differentiable_in x0 & diff ((f1 + f2),x0) = (diff (f1,x0)) + (diff (f2,x0)) ) )

reconsider j = 1 as Element of REAL by XREAL_0:def 1;

assume that

A1: f1 is_differentiable_in x0 and

A2: f2 is_differentiable_in x0 ; :: thesis: ( f1 + f2 is_differentiable_in x0 & diff ((f1 + f2),x0) = (diff (f1,x0)) + (diff (f2,x0)) )

consider N1 being Neighbourhood of x0 such that

A3: N1 c= dom f1 and

A4: ex L being LinearFunc ex R being RestFunc st

for x being Real st x in N1 holds

(f1 . x) - (f1 . x0) = (L . (x - x0)) + (R . (x - x0)) by A1;

consider L1 being LinearFunc, R1 being RestFunc such that

A5: for x being Real st x in N1 holds

(f1 . x) - (f1 . x0) = (L1 . (x - x0)) + (R1 . (x - x0)) by A4;

consider N2 being Neighbourhood of x0 such that

A6: N2 c= dom f2 and

A7: ex L being LinearFunc ex R being RestFunc st

for x being Real st x in N2 holds

(f2 . x) - (f2 . x0) = (L . (x - x0)) + (R . (x - x0)) by A2;

consider L2 being LinearFunc, R2 being RestFunc such that

A8: for x being Real st x in N2 holds

(f2 . x) - (f2 . x0) = (L2 . (x - x0)) + (R2 . (x - x0)) by A7;

reconsider R = R1 + R2 as RestFunc by Th4;

reconsider L = L1 + L2 as LinearFunc by Th2;

A9: ( L1 is total & L2 is total ) by Def3;

consider N being Neighbourhood of x0 such that

A10: N c= N1 and

A11: N c= N2 by RCOMP_1:17;

A12: N c= dom f2 by A6, A11;

N c= dom f1 by A3, A10;

then N /\ N c= (dom f1) /\ (dom f2) by A12, XBOOLE_1:27;

then A13: N c= dom (f1 + f2) by VALUED_1:def 1;

A14: ( R1 is total & R2 is total ) by Def2;

A15: now :: thesis: for x being Real st x in N holds

((f1 + f2) . x) - ((f1 + f2) . x0) = (L . (x - x0)) + (R . (x - x0))

hence
f1 + f2 is_differentiable_in x0
by A13; :: thesis: diff ((f1 + f2),x0) = (diff (f1,x0)) + (diff (f2,x0))((f1 + f2) . x) - ((f1 + f2) . x0) = (L . (x - x0)) + (R . (x - x0))

let x be Real; :: thesis: ( x in N implies ((f1 + f2) . x) - ((f1 + f2) . x0) = (L . (x - x0)) + (R . (x - x0)) )

A16: x0 in N by RCOMP_1:16;

reconsider xx = x, xx0 = x0 as Element of REAL by XREAL_0:def 1;

assume A17: x in N ; :: thesis: ((f1 + f2) . x) - ((f1 + f2) . x0) = (L . (x - x0)) + (R . (x - x0))

hence ((f1 + f2) . x) - ((f1 + f2) . x0) = ((f1 . x) + (f2 . x)) - ((f1 + f2) . x0) by A13, VALUED_1:def 1

.= ((f1 . x) + (f2 . x)) - ((f1 . x0) + (f2 . x0)) by A13, A16, VALUED_1:def 1

.= ((f1 . x) - (f1 . x0)) + ((f2 . x) - (f2 . x0))

.= ((L1 . (x - x0)) + (R1 . (x - x0))) + ((f2 . x) - (f2 . x0)) by A5, A10, A17

.= ((L1 . (x - x0)) + (R1 . (x - x0))) + ((L2 . (x - x0)) + (R2 . (x - x0))) by A8, A11, A17

.= ((L1 . (x - x0)) + (L2 . (x - x0))) + ((R1 . (x - x0)) + (R2 . (x - x0)))

.= (L . (x - x0)) + ((R1 . (xx - xx0)) + (R2 . (xx - xx0))) by A9, RFUNCT_1:56

.= (L . (x - x0)) + (R . (x - x0)) by A14, RFUNCT_1:56 ;

:: thesis: verum

end;A16: x0 in N by RCOMP_1:16;

reconsider xx = x, xx0 = x0 as Element of REAL by XREAL_0:def 1;

assume A17: x in N ; :: thesis: ((f1 + f2) . x) - ((f1 + f2) . x0) = (L . (x - x0)) + (R . (x - x0))

hence ((f1 + f2) . x) - ((f1 + f2) . x0) = ((f1 . x) + (f2 . x)) - ((f1 + f2) . x0) by A13, VALUED_1:def 1

.= ((f1 . x) + (f2 . x)) - ((f1 . x0) + (f2 . x0)) by A13, A16, VALUED_1:def 1

.= ((f1 . x) - (f1 . x0)) + ((f2 . x) - (f2 . x0))

.= ((L1 . (x - x0)) + (R1 . (x - x0))) + ((f2 . x) - (f2 . x0)) by A5, A10, A17

.= ((L1 . (x - x0)) + (R1 . (x - x0))) + ((L2 . (x - x0)) + (R2 . (x - x0))) by A8, A11, A17

.= ((L1 . (x - x0)) + (L2 . (x - x0))) + ((R1 . (x - x0)) + (R2 . (x - x0)))

.= (L . (x - x0)) + ((R1 . (xx - xx0)) + (R2 . (xx - xx0))) by A9, RFUNCT_1:56

.= (L . (x - x0)) + (R . (x - x0)) by A14, RFUNCT_1:56 ;

:: thesis: verum

hence diff ((f1 + f2),x0) = L . 1 by A13, A15, Def5

.= (L1 . j) + (L2 . j) by A9, RFUNCT_1:56

.= (diff (f1,x0)) + (L2 . 1) by A1, A3, A5, Def5

.= (diff (f1,x0)) + (diff (f2,x0)) by A2, A6, A8, Def5 ;

:: thesis: verum