theorem :: INTEGR19:15

for n being Element of NAT
for A being non empty closed_interval Subset of REAL
for f being PartFunc of REAL,(REAL n) st f is bounded & A c= dom f holds
f | A is bounded