theorem Th16: :: INTEGR19:16

for n being Element of NAT
for A being non empty closed_interval Subset of REAL
for f being PartFunc of REAL,(REAL n)
for g being Function of A,(REAL n) st f is bounded & f = g holds
g is bounded ;