let A be non empty closed_interval Subset of REAL; :: thesis: for r being Real ex f being Function of A,REAL st
( rng f = {r} & f | A is bounded )
let r be Real; :: thesis: ex f being Function of A,REAL st
( rng f = {r} & f | A is bounded )
r (#) (chi (A,A)) is total by Th3;
then reconsider f = r (#) (chi (A,A)) as Function of A,REAL ;
A1: rng f = {r} by Th3;
then A2: f | A is bounded_below by INTEGRA1:12;
f | A is bounded_above by A1, INTEGRA1:14;
hence ex f being Function of A,REAL st
( rng f = {r} & f | A is bounded ) by A1, A2; :: thesis: verum