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 )
assume A1: ( a <= b & ['a,b'] c= dom f ) ; :: thesis: ||.f.|| | ['a,b'] is bounded
P11: f | ['a,b'] is continuous ;
['a,b'] c= dom ||.f.|| by NORMSP_0:def 3, A1;
hence ||.f.|| | ['a,b'] is bounded by P11, A1, NFCONT_3:22, INTEGRA5:10; :: thesis: verum