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