theorem Th1915: :: INTEGR21:1

for Z being RealNormSpace
for A being non empty closed_interval Subset of REAL
for f being PartFunc of REAL, the carrier of Z st f is bounded & A c= dom f holds
f | A is bounded