theorem :: FUZZY_7:14

for s being Real
for f, g being Function of REAL,REAL holds
( dom ((f | ].-infty,s.]) +* (g | [.s,+infty.[)) = REAL & dom ((f | ].-infty,s.[) +* (g | [.s,+infty.[)) = REAL )