let X be non empty closed_interval Subset of REAL; :: thesis: for Y being RealNormSpace
for f being continuous PartFunc of REAL,Y st dom f = X holds
f is bounded Function of X,Y
let Y be RealNormSpace; :: thesis: for f being continuous PartFunc of REAL,Y st dom f = X holds
f is bounded Function of X,Y
let f be continuous PartFunc of REAL,Y; :: thesis: ( dom f = X implies f is bounded Function of X,Y )
assume A1: dom f = X ; :: thesis: f is bounded Function of X,Y
rng f c= the carrier of Y ;
then reconsider g = f as Function of X,Y by A1, FUNCT_2:2;
f | X = f by A1;
then A2: ||.f.|| | X is continuous by A1, NFCONT_3:22;
A3: dom ||.f.|| = X by A1, NORMSP_0:def 2;
then consider x1, x2 being Real such that
A4: ( x1 in dom ||.f.|| & x2 in dom ||.f.|| & ||.f.|| . x1 = upper_bound (rng ||.f.||) & ||.f.|| . x2 = lower_bound (rng ||.f.||) ) by A2, FCONT_1:30;
A5: ||.f.|| . x1 = ||.(f /. x1).|| by A4, NORMSP_0:def 2;
reconsider K = ||.f.|| . x1 as Real ;

now :: thesis: for x being Element of X holds ||.(g . x).|| <= K

let x be Element of X; :: thesis: ||.(g . x).|| <= K
A6: ||.(g . x).|| = ||.(g /. x).||
.= ||.f.|| . x by A3, NORMSP_0:def 2
.= ||.f.|| /. x by A3, PARTFUN1:def 6 ;
A7: rng ||.f.|| is real-bounded by A2, A3, FCONT_1:28, RCOMP_1:10;
||.f.|| . x in rng ||.f.|| by A3, FUNCT_1:3;
then ||.f.|| /. x in rng ||.f.|| by A3, PARTFUN1:def 6;
hence ||.(g . x).|| <= K by A4, A6, A7, SEQ_4:def 1; :: thesis: verum

end;

hence f is bounded Function of X,Y by A5, RSSPACE4:def 4; :: thesis: verum