theorem :: FUZZY_8:8

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