let a, b be Real; 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; 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; ( 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 )
; 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 ;
( y in dom (f | ['a,b']) implies ||.((f | ['a,b']) /. y).|| < r )
assume P3:
y in dom (f | ['a,b'])
;
||.((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;
verum
end;
hence
f | ['a,b'] is bounded
; verum