let Z be RealNormSpace; :: thesis: 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
let A, B be non empty closed_interval Subset of REAL; :: thesis: 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
let f be PartFunc of REAL, the carrier of Z; :: thesis: ( f | A is bounded & B c= A & B c= dom (f | A) implies f | B is bounded )
assume A1: ( f | A is bounded & B c= A & B c= dom (f | A) ) ; :: thesis: f | B is bounded
set g = f | A;
A4: (f | A) | B is bounded by Th1915, A1;
consider r being Real such that
A5: for x being set st x in dom ((f | A) | B) holds
||.(((f | A) | B) /. x).|| < r by A4;
(f | A) | B = f | B by A1, RELAT_1:74;
hence f | B is bounded by A5; :: thesis: verum