let A be 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:14;
f | A is bounded_above by A1, INTEGRA1:16;
hence ex f being Function of A,REAL st
( rng f = {r} & f | A is bounded ) by A1, A2; :: thesis: verum