theorem FUZZY711: :: FUZZY_8:15

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