let p, g be Real; :: thesis: ( p < g implies for f1, f2 being PartFunc of REAL ,REAL st f1 is_differentiable_on ].p,g.[ & f2 is_differentiable_on ].p,g.[ & ( for x being Real st x in ].p,g.[ holds
diff f1,x = diff f2,x ) holds
( (f1 - f2) | ].p,g.[ is V8() & ex r being Real st
for x being Real st x in ].p,g.[ holds
f1 . x = (f2 . x) + r ) )
assume A1: p < g ; :: thesis: for f1, f2 being PartFunc of REAL ,REAL st f1 is_differentiable_on ].p,g.[ & f2 is_differentiable_on ].p,g.[ & ( for x being Real st x in ].p,g.[ holds
diff f1,x = diff f2,x ) holds
( (f1 - f2) | ].p,g.[ is V8() & ex r being Real st
for x being Real st x in ].p,g.[ holds
f1 . x = (f2 . x) + r )
let f1, f2 be PartFunc of REAL ,REAL ; :: thesis: ( f1 is_differentiable_on ].p,g.[ & f2 is_differentiable_on ].p,g.[ & ( for x being Real st x in ].p,g.[ holds
diff f1,x = diff f2,x ) implies ( (f1 - f2) | ].p,g.[ is V8() & ex r being Real st
for x being Real st x in ].p,g.[ holds
f1 . x = (f2 . x) + r ) )
assume that
A2: f1 is_differentiable_on ].p,g.[ and
A3: f2 is_differentiable_on ].p,g.[ and
A4: for x being Real st x in ].p,g.[ holds
diff f1,x = diff f2,x ; :: thesis: ( (f1 - f2) | ].p,g.[ is V8() & ex r being Real st
for x being Real st x in ].p,g.[ holds
f1 . x = (f2 . x) + r )
reconsider Z = ].p,g.[ as open Subset of REAL ;
A5: ].p,g.[ c= dom f1 by A2, FDIFF_1:def 7;
].p,g.[ c= dom f2 by A3, FDIFF_1:def 7;
then ].p,g.[ c= (dom f1) /\ (dom f2) by A5, XBOOLE_1:19;
then A6: ].p,g.[ c= dom (f1 - f2) by VALUED_1:12;
then A7: ( f1 - f2 is_differentiable_on Z & ( for x being Real st x in Z holds
((f1 - f2) `| Z) . x = (diff f1,x) - (diff f2,x) ) ) by A2, A3, FDIFF_1:27;

now

let x be Real; :: thesis: ( x in ].p,g.[ implies diff (f1 - f2),x = 0 )
assume A8: x in ].p,g.[ ; :: thesis: diff (f1 - f2),x = 0
hence diff (f1 - f2),x = ((f1 - f2) `| Z) . x by A7, FDIFF_1:def 8
.= (diff f1,x) - (diff f2,x) by A2, A3, A6, A8, FDIFF_1:27
.= (diff f1,x) - (diff f1,x) by A4, A8
.= 0 ;
:: thesis: verum

end;

hence (f1 - f2) | ].p,g.[ is V8() by A1, A6, Th7, A2, A3, FDIFF_1:27; :: thesis: ex r being Real st
for x being Real st x in ].p,g.[ holds
f1 . x = (f2 . x) + r
then consider r being Real such that
A9: for x being Real st x in ].p,g.[ /\ (dom (f1 - f2)) holds
(f1 - f2) . x = r by PARTFUN2:76;
take r ; :: thesis: for x being Real st x in ].p,g.[ holds
f1 . x = (f2 . x) + r
let x be Real; :: thesis: ( x in ].p,g.[ implies f1 . x = (f2 . x) + r )
assume A10: x in ].p,g.[ ; :: thesis: f1 . x = (f2 . x) + r
then x in ].p,g.[ /\ (dom (f1 - f2)) by A6, XBOOLE_1:28;
then r = (f1 - f2) . x by A9
.= (f1 . x) - (f2 . x) by A6, A10, VALUED_1:13 ;
hence f1 . x = (f2 . x) + r ; :: thesis: verum