let a, b be Real; :: thesis: for Y being RealNormSpace
for f being continuous PartFunc of REAL, the carrier of Y st a <= b & ['a,b'] c= dom f holds
f | ['a,b'] is bounded
let Y be RealNormSpace; :: thesis: for f being continuous PartFunc of REAL, the carrier of Y st a <= b & ['a,b'] c= dom f holds
f | ['a,b'] is bounded
let f be continuous PartFunc of REAL, the carrier of Y; :: thesis: ( a <= b & ['a,b'] c= dom f implies f | ['a,b'] is bounded )
set h = ||.f.|| | ['a,b'];
set g = f | ['a,b'];
assume A1: ( a <= b & ['a,b'] c= dom f ) ; :: thesis: f | ['a,b'] is bounded
then ||.f.|| | ['a,b'] is bounded by Th3;
then consider r being Real such that
P2: for y being set st y in dom (||.f.|| | ['a,b']) holds
|.((||.f.|| | ['a,b']) . y).| < r by COMSEQ_2:def 3;
D1: dom ||.f.|| = dom f by NORMSP_0:def 3;
for y being set st y in dom (f | ['a,b']) holds
||.((f | ['a,b']) /. y).|| < r

proof

let y be set ; :: thesis: ( y in dom (f | ['a,b']) implies ||.((f | ['a,b']) /. y).|| < r )
assume P3: y in dom (f | ['a,b']) ; :: thesis: ||.((f | ['a,b']) /. y).|| < r
then P5: y in ['a,b'] by A1, RELAT_1:62;
then P6: y in dom (||.f.|| | ['a,b']) by A1, D1, RELAT_1:62;
P81: (||.f.|| | ['a,b']) . y = ||.f.|| . y by P5, FUNCT_1:49
.= ||.(f /. y).|| by NORMSP_0:def 2, D1, P5, A1 ;
f /. y = f . y by PARTFUN1:def 6, P5, A1
.= (f | ['a,b']) . y by P5, FUNCT_1:49
.= (f | ['a,b']) /. y by PARTFUN1:def 6, P3 ;
then |.((||.f.|| | ['a,b']) . y).| = ||.((f | ['a,b']) /. y).|| by P81, ABSVALUE:def 1;
hence ||.((f | ['a,b']) /. y).|| < r by P2, P6; :: thesis: verum

end;

hence f | ['a,b'] is bounded ; :: thesis: verum