theorem Th4: :: INTEGR21:12

for a, b being 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.|| is_integrable_on ['a,b']