theorem Th1915a: :: INTEGR21:2

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