theorem Lm3: :: FUZZY_6:6

for A being non empty closed_interval Subset of REAL
for f being Function of REAL,REAL st f is_integrable_on A & f | A is bounded holds
( (id REAL) (#) f is_integrable_on A & ((id REAL) (#) f) | A is bounded )