theorem :: FUZZY_9:34

for A being non empty closed_interval Subset of REAL
for a being Real
for f, g being Function of REAL,REAL st f | A is bounded & g | A is bounded & a in A holds
( ((f | ].-infty,a.[) +* (g | [.a,+infty.[)) | ['(lower_bound A),a'] is bounded & ((f | ].-infty,a.[) +* (g | [.a,+infty.[)) | ['a,(upper_bound A)'] is bounded )