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.|| is_integrable_on ['a,b']
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.|| is_integrable_on ['a,b']
let f be continuous PartFunc of REAL, the carrier of Y; :: thesis: ( a <= b & ['a,b'] c= dom f implies ||.f.|| is_integrable_on ['a,b'] )
assume A1: ( a <= b & ['a,b'] c= dom f ) ; :: thesis: ||.f.|| is_integrable_on ['a,b']
P11: f | ['a,b'] is continuous ;
['a,b'] c= dom ||.f.|| by NORMSP_0:def 3, A1;
hence ||.f.|| is_integrable_on ['a,b'] by P11, A1, NFCONT_3:22, INTEGRA5:11; :: thesis: verum