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 that
A1: f1 is_differentiable_on A and
A2: f2 is_differentiable_on A ; :: thesis: ( f1 + f2 is_differentiable_on A & (f1 + f2) `| A = (f1 `| A) + (f2 `| A) )
A3: A c= dom f2 by A2;
A c= dom f1 by A1;
then A c= (dom f1) /\ (dom f2) by A3, XBOOLE_1:19;
then A4: A c= dom (f1 + f2) by VALUED_1:def 1;
then f1 + f2 is_differentiable_on A by A1, A2, FDIFF_1:18;
then A5: dom ((f1 + f2) `| A) = A by FDIFF_1:def 7;
A6: dom (f2 `| A) = A by A2, FDIFF_1:def 7;
dom (f1 `| A) = A by A1, FDIFF_1:def 7;
then (dom (f1 `| A)) /\ (dom (f2 `| A)) = A by A6;
then A7: dom ((f1 `| A) + (f2 `| A)) = A by VALUED_1:def 1;

now :: thesis: for x0 being Element of REAL st x0 in A holds
((f1 + f2) `| A) . x0 = ((f1 `| A) + (f2 `| A)) . x0

let x0 be Element of REAL ; :: thesis: ( x0 in A implies ((f1 + f2) `| A) . x0 = ((f1 `| A) + (f2 `| A)) . x0 )
assume A8: 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, A2, A4, FDIFF_1:18
.= ((f1 `| A) . x0) + (diff (f2,x0)) by A1, A8, FDIFF_1:def 7
.= ((f1 `| A) . x0) + ((f2 `| A) . x0) by A2, A8, FDIFF_1:def 7
.= ((f1 `| A) + (f2 `| A)) . x0 by A7, A8, VALUED_1:def 1 ;
:: thesis: verum

end;

hence ( f1 + f2 is_differentiable_on A & (f1 + f2) `| A = (f1 `| A) + (f2 `| A) ) by A1, A2, A4, A5, A7, FDIFF_1:18, PARTFUN1:5; :: thesis: verum