let p, g be Real; :: 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 constant & 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 constant & ex r being Real st
for x being Real st x in ].p,g.[ holds
f1 . x = (f2 . x) + r ) )
assume that
A1: ( f1 is_differentiable_on ].p,g.[ & f2 is_differentiable_on ].p,g.[ ) and
A2: for x being Real st x in ].p,g.[ holds
diff (f1,x) = diff (f2,x) ; :: thesis: ( (f1 - f2) | ].p,g.[ is constant & 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 ;
( ].p,g.[ c= dom f1 & ].p,g.[ c= dom f2 ) by A1, FDIFF_1:def 6;
then ].p,g.[ c= (dom f1) /\ (dom f2) by XBOOLE_1:19;
then A3: ].p,g.[ c= dom (f1 - f2) by VALUED_1:12;
then A4: f1 - f2 is_differentiable_on Z by A1, FDIFF_1:19;

now :: thesis: for x being Real st x in ].p,g.[ holds
diff ((f1 - f2),x) = 0

let x be Real; :: thesis: ( x in ].p,g.[ implies diff ((f1 - f2),x) = 0 )
assume A5: x in ].p,g.[ ; :: thesis: diff ((f1 - f2),x) = 0
hence diff ((f1 - f2),x) = ((f1 - f2) `| Z) . x by A4, FDIFF_1:def 7
.= (diff (f1,x)) - (diff (f2,x)) by A1, A3, A5, FDIFF_1:19
.= (diff (f1,x)) - (diff (f1,x)) by A2, A5
.= 0 ;
:: thesis: verum

end;

hence (f1 - f2) | ].p,g.[ is constant by A1, A3, Th7, FDIFF_1:19; :: 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 Element of REAL such that
A6: for x being Element of REAL st x in ].p,g.[ /\ (dom (f1 - f2)) holds
(f1 - f2) . x = r by PARTFUN2:57;
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 A7: x in ].p,g.[ ; :: thesis: f1 . x = (f2 . x) + r
then x in ].p,g.[ /\ (dom (f1 - f2)) by A3, XBOOLE_1:28;
then r = (f1 - f2) . x by A6
.= (f1 . x) - (f2 . x) by A3, A7, VALUED_1:13 ;
hence f1 . x = (f2 . x) + r ; :: thesis: verum