theorem :: FUZZY_6:37
for a, b, c being Real
for f, g being Function of REAL,REAL st a <= c & c <= b holds
(f | [.a,c.[) +* (g | [.c,b.]) = (f | [.a,c.]) +* (g | [.c,b.])