for f1, f2 being Function of [:I[01],I[01]:],I[01] st f1 is continuous & f2 is continuous & ( for p being Point of [:I[01],I[01]:] holds (f1 . p) - (f2 . p) is Point of I[01] ) holds
ex g being Function of [:I[01],I[01]:],I[01] st
( ( for p being Point of [:I[01],I[01]:]
for r1, r2 being Real st f1 . p = r1 & f2 . p = r2 holds
g . p = r1 - r2 ) & g is continuous )