let f1, f2 be PartFunc of REAL,REAL; :: thesis: for I being non empty Interval st I c= dom (f1 - f2) & f1 is_differentiable_on_interval I & f2 is_differentiable_on_interval I holds
( f1 - f2 is_differentiable_on_interval I & (f1 - f2) `\ I = (f1 `\ I) - (f2 `\ I) & ( for x being Real st x in I holds
((f1 - f2) `\ I) . x = ((f1 `\ I) . x) - ((f2 `\ I) . x) ) )
let I be non empty Interval; :: thesis: ( I c= dom (f1 - f2) & f1 is_differentiable_on_interval I & f2 is_differentiable_on_interval I implies ( f1 - f2 is_differentiable_on_interval I & (f1 - f2) `\ I = (f1 `\ I) - (f2 `\ I) & ( for x being Real st x in I holds
((f1 - f2) `\ I) . x = ((f1 `\ I) . x) - ((f2 `\ I) . x) ) ) )
assume that
A1: I c= dom (f1 - f2) and
A2: f1 is_differentiable_on_interval I and
A3: f2 is_differentiable_on_interval I ; :: thesis: ( f1 - f2 is_differentiable_on_interval I & (f1 - f2) `\ I = (f1 `\ I) - (f2 `\ I) & ( for x being Real st x in I holds
((f1 - f2) `\ I) . x = ((f1 `\ I) . x) - ((f2 `\ I) . x) ) )
reconsider J = ].(inf I),(sup I).[ as open Subset of REAL by Th2;
J c= I by Th2;
then A4: J c= dom (f1 - f2) by A1;
A5: for x being Real st x in J holds
(f1 - f2) | J is_differentiable_in x

proof

let x be Real; :: thesis: ( x in J implies (f1 - f2) | J is_differentiable_in x )
assume x in J ; :: thesis: (f1 - f2) | J is_differentiable_in x
then ( f1 | J is_differentiable_in x & f2 | J is_differentiable_in x ) by A2, A3, FDIFF_1:def 6;
then (f1 | J) - (f2 | J) is_differentiable_in x by FDIFF_1:14;
hence (f1 - f2) | J is_differentiable_in x by RFUNCT_1:47; :: thesis: verum

end;

hence A6: f1 - f2 is_differentiable_on_interval I by A1, A4, A2, A3, FDIFF_3:11, FDIFF_3:17, FDIFF_1:def 6; :: thesis: ( (f1 - f2) `\ I = (f1 `\ I) - (f2 `\ I) & ( for x being Real st x in I holds
((f1 - f2) `\ I) . x = ((f1 `\ I) . x) - ((f2 `\ I) . x) ) )
then A7: dom ((f1 - f2) `\ I) = I by Def2;
( dom (f1 `\ I) = I & dom (f2 `\ I) = I ) by A2, A3, Def2;
then A8: dom ((f1 `\ I) - (f2 `\ I)) = I /\ I by VALUED_1:12;
A9: for x being Element of REAL st x in dom ((f1 - f2) `\ I) holds
((f1 - f2) `\ I) . x = ((f1 `\ I) - (f2 `\ I)) . x

proof

let x be Element of REAL ; :: thesis: ( x in dom ((f1 - f2) `\ I) implies ((f1 - f2) `\ I) . x = ((f1 `\ I) - (f2 `\ I)) . x )
assume A10: x in dom ((f1 - f2) `\ I) ; :: thesis: ((f1 - f2) `\ I) . x = ((f1 `\ I) - (f2 `\ I)) . x
then A11: x in I by A6, Def2;

per cases ( x = inf I or x = sup I or ( x <> inf I & x <> sup I ) ) ;

suppose A12: x = inf I ; :: thesis: ((f1 - f2) `\ I) . x = ((f1 `\ I) - (f2 `\ I)) . x

then A13: inf I = lower_bound I by A11, Lm5;
( (f1 `\ I) . x = Rdiff (f1,x) & (f2 `\ I) . x = Rdiff (f2,x) & ((f1 - f2) `\ I) . x = Rdiff ((f1 - f2),x) ) by A2, A3, A6, A11, A12, Def2;
then ((f1 - f2) `\ I) . x = ((f1 `\ I) . x) - ((f2 `\ I) . x) by A10, A6, Def2, A12, A13, A2, A3, FDIFF_3:17;
hence ((f1 - f2) `\ I) . x = ((f1 `\ I) - (f2 `\ I)) . x by A7, A8, A10, VALUED_1:13; :: thesis: verum

end;

suppose A14: x = sup I ; :: thesis: ((f1 - f2) `\ I) . x = ((f1 `\ I) - (f2 `\ I)) . x

then A15: sup I = upper_bound I by A11, Lm6;
( (f1 `\ I) . x = Ldiff (f1,x) & (f2 `\ I) . x = Ldiff (f2,x) & ((f1 - f2) `\ I) . x = Ldiff ((f1 - f2),x) ) by A2, A3, A6, A11, A14, Def2;
then ((f1 - f2) `\ I) . x = ((f1 `\ I) . x) - ((f2 `\ I) . x) by A10, A6, Def2, A14, A15, A2, A3, FDIFF_3:11;
hence ((f1 - f2) `\ I) . x = ((f1 `\ I) - (f2 `\ I)) . x by A7, A8, A10, VALUED_1:13; :: thesis: verum

end;

suppose A16: ( x <> inf I & x <> sup I ) ; :: thesis: ((f1 - f2) `\ I) . x = ((f1 `\ I) - (f2 `\ I)) . x

A17: ( (f1 `\ I) . x = diff (f1,x) & (f2 `\ I) . x = diff (f2,x) & ((f1 - f2) `\ I) . x = diff ((f1 - f2),x) ) by A16, A11, A2, A3, A6, Def2;
( inf I <= x & x <= sup I ) by A11, XXREAL_2:61, XXREAL_2:62;
then A18: ( inf I < x & x < sup I ) by A16, XXREAL_0:1;
then A19: x in J by XXREAL_1:4;
A20: ((f1 - f2) `| J) . x = (diff (f1,x)) - (diff (f2,x)) by A2, A3, A4, A18, FDIFF_1:19, XXREAL_1:4;
( f1 is_differentiable_on J & f2 is_differentiable_on J & f1 - f2 is_differentiable_on J ) by A2, A3, A5, A4;
then ((f1 - f2) `\ I) . x = ((f1 `\ I) . x) - ((f2 `\ I) . x) by A17, A19, A20, FDIFF_1:def 7;
hence ((f1 - f2) `\ I) . x = ((f1 `\ I) - (f2 `\ I)) . x by A7, A8, A10, VALUED_1:13; :: thesis: verum

end;

end;

end;

hence (f1 - f2) `\ I = (f1 `\ I) - (f2 `\ I) by A7, A8, PARTFUN1:5; :: thesis: for x being Real st x in I holds
((f1 - f2) `\ I) . x = ((f1 `\ I) . x) - ((f2 `\ I) . x)

hereby :: thesis: verum

let x be Real; :: thesis: ( x in I implies ((f1 - f2) `\ I) . x = ((f1 `\ I) . x) - ((f2 `\ I) . x) )
assume A21: x in I ; :: thesis: ((f1 - f2) `\ I) . x = ((f1 `\ I) . x) - ((f2 `\ I) . x)
then ((f1 - f2) `\ I) . x = ((f1 `\ I) - (f2 `\ I)) . x by A7, A9;
hence ((f1 - f2) `\ I) . x = ((f1 `\ I) . x) - ((f2 `\ I) . x) by A21, A8, VALUED_1:13; :: thesis: verum

end;