let A be open Subset of REAL ; :: thesis: for f1, f2 being PartFunc of REAL ,REAL st f1 is_differentiable_on A & f2 is_differentiable_on A holds
( f1 + f2 is_differentiable_on A & (f1 + f2) `| A = (f1 `| A) + (f2 `| A) )
let f1, f2 be PartFunc of REAL ,REAL ; :: thesis: ( f1 is_differentiable_on A & f2 is_differentiable_on A implies ( f1 + f2 is_differentiable_on A & (f1 + f2) `| A = (f1 `| A) + (f2 `| A) ) )
assume A1: ( f1 is_differentiable_on A & f2 is_differentiable_on A ) ; :: thesis: ( f1 + f2 is_differentiable_on A & (f1 + f2) `| A = (f1 `| A) + (f2 `| A) )
then A2: A c= dom f1 by FDIFF_1:def 7;
A c= dom f2 by A1, FDIFF_1:def 7;
then A c= (dom f1) /\ (dom f2) by A2, XBOOLE_1:19;
then A3: A c= dom (f1 + f2) by VALUED_1:def 1;
then ( f1 + f2 is_differentiable_on A & ( for x0 being Real st x0 in A holds
((f1 + f2) `| A) . x0 = (diff f1,x0) + (diff f2,x0) ) ) by A1, FDIFF_1:26;
then A4: dom ((f1 + f2) `| A) = A by FDIFF_1:def 8;
A5: dom (f1 `| A) = A by A1, FDIFF_1:def 8;
dom (f2 `| A) = A by A1, FDIFF_1:def 8;
then (dom (f1 `| A)) /\ (dom (f2 `| A)) = A by A5;
then A6: dom ((f1 `| A) + (f2 `| A)) = A by VALUED_1:def 1;

now

let x0 be Real; :: thesis: ( x0 in A implies ((f1 + f2) `| A) . x0 = ((f1 `| A) + (f2 `| A)) . x0 )
assume A7: x0 in A ; :: thesis: ((f1 + f2) `| A) . x0 = ((f1 `| A) + (f2 `| A)) . x0
hence ((f1 + f2) `| A) . x0 = (diff f1,x0) + (diff f2,x0) by A1, A3, FDIFF_1:26
.= ((f1 `| A) . x0) + (diff f2,x0) by A1, A7, FDIFF_1:def 8
.= ((f1 `| A) . x0) + ((f2 `| A) . x0) by A1, A7, FDIFF_1:def 8
.= ((f1 `| A) + (f2 `| A)) . x0 by A6, A7, VALUED_1:def 1 ;
:: thesis: verum

end;

hence ( f1 + f2 is_differentiable_on A & (f1 + f2) `| A = (f1 `| A) + (f2 `| A) ) by A1, A3, A4, A6, FDIFF_1:26, PARTFUN1:34; :: thesis: verum