for p, g being Real
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 )