let A be non empty closed_interval Subset of REAL; :: thesis: for X being set
for f being PartFunc of A,REAL st f | A is bounded_above holds
rng (f | X) is bounded_above
let X be set ; :: thesis: for f being PartFunc of A,REAL st f | A is bounded_above holds
rng (f | X) is bounded_above
let f be PartFunc of A,REAL; :: thesis: ( f | A is bounded_above implies rng (f | X) is bounded_above )
assume f | A is bounded_above ; :: thesis: rng (f | X) is bounded_above
then rng f is bounded_above by INTEGRA1:13;
hence rng (f | X) is bounded_above by RELAT_1:70, XXREAL_2:43; :: thesis: verum