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

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