theorem Th20: :: INTEGR26:20

for p, q being R_eal
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 )