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, FDIFF_1:def 7;
A c= dom f1 by A1, FDIFF_1:def 7;
then A c= (dom f1) /\ (dom f2) by A3, XBOOLE_1:19;
then A4: A c= dom (f1 - f2) by VALUED_1:12;
then f1 - f2 is_differentiable_on A by A1, A2, FDIFF_1:27;
then A5: dom ((f1 - f2) `| A) = A by FDIFF_1:def 8;
A6: dom (f2 `| A) = A by A2, FDIFF_1:def 8;
dom (f1 `| A) = A by A1, FDIFF_1:def 8;
then (dom (f1 `| A)) /\ (dom (f2 `| A)) = A by A6;
then A7: dom ((f1 `| A) - (f2 `| A)) = A by VALUED_1:12;

now

let x0 be 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:27
.= ((f1 `| A) . x0) - (diff f2,x0) by A1, A8, FDIFF_1:def 8
.= ((f1 `| A) . x0) - ((f2 `| A) . x0) by A2, A8, FDIFF_1:def 8
.= ((f1 `| A) - (f2 `| A)) . x0 by A7, A8, VALUED_1:13 ;
:: 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:27, PARTFUN1:34; :: thesis: verum