let p, q be R_eal; :: thesis: for f1, f2 being PartFunc of REAL,REAL st f1 is_differentiable_on ].p,q.[ & f2 is_differentiable_on ].p,q.[ & ( for x being Real st x in ].p,q.[ holds
diff (f1,x) = diff (f2,x) ) holds
( (f1 - f2) | ].p,q.[ is constant & ex r being Real st
for x being Real st x in ].p,q.[ holds
f1 . x = (f2 . x) + r )
let f1, f2 be PartFunc of REAL,REAL; :: thesis: ( f1 is_differentiable_on ].p,q.[ & f2 is_differentiable_on ].p,q.[ & ( for x being Real st x in ].p,q.[ holds
diff (f1,x) = diff (f2,x) ) implies ( (f1 - f2) | ].p,q.[ is constant & ex r being Real st
for x being Real st x in ].p,q.[ holds
f1 . x = (f2 . x) + r ) )
assume that
A1: ( f1 is_differentiable_on ].p,q.[ & f2 is_differentiable_on ].p,q.[ ) and
A2: for x being Real st x in ].p,q.[ holds
diff (f1,x) = diff (f2,x) ; :: thesis: ( (f1 - f2) | ].p,q.[ is constant & ex r being Real st
for x being Real st x in ].p,q.[ holds
f1 . x = (f2 . x) + r )
].p,q.[ is open_interval by MEASURE5:def 2;
then reconsider Z = ].p,q.[ as open Subset of REAL ;
].p,q.[ c= (dom f1) /\ (dom f2) by A1, XBOOLE_1:19;
then A3: ].p,q.[ 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,q.[ holds
diff ((f1 - f2),x) = 0

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

end;

then A6: (f1 - f2) | Z is constant by A1, A3, Th19, FDIFF_1:19;
hence (f1 - f2) | ].p,q.[ is constant ; :: thesis: ex r being Real st
for x being Real st x in ].p,q.[ holds
f1 . x = (f2 . x) + r
consider r being Element of REAL such that
A7: for x being Element of REAL st x in ].p,q.[ /\ (dom (f1 - f2)) holds
(f1 - f2) . x = r by A6, PARTFUN2:57;
take r ; :: thesis: for x being Real st x in ].p,q.[ holds
f1 . x = (f2 . x) + r
let x be Real; :: thesis: ( x in ].p,q.[ implies f1 . x = (f2 . x) + r )
assume A8: x in ].p,q.[ ; :: thesis: f1 . x = (f2 . x) + r
then x in ].p,q.[ /\ (dom (f1 - f2)) by A3, XBOOLE_1:28;
then r = (f1 - f2) . x by A7;
then r = (f1 . x) - (f2 . x) by A3, A8, VALUED_1:13;
hence f1 . x = (f2 . x) + r ; :: thesis: verum