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

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