let Z be RealNormSpace; :: thesis: for A being non empty closed_interval Subset of REAL
for f being PartFunc of REAL, the carrier of Z st f is bounded & A c= dom f holds
f | A is bounded
let A be non empty closed_interval Subset of REAL; :: thesis: for f being PartFunc of REAL, the carrier of Z st f is bounded & A c= dom f holds
f | A is bounded
let f be PartFunc of REAL, the carrier of Z; :: thesis: ( f is bounded & A c= dom f implies f | A is bounded )
assume that
A1: f is bounded and
A2: A c= dom f ; :: thesis: f | A is bounded
consider r being Real such that
A3: for x being set st x in dom f holds
||.(f /. x).|| < r by A1;

now :: thesis: for x being set st x in dom (f | A) holds
||.((f | A) /. x).|| < r

let x be set ; :: thesis: ( x in dom (f | A) implies ||.((f | A) /. x).|| < r )
assume x in dom (f | A) ; :: thesis: ||.((f | A) /. x).|| < r
then ( ||.(f /. x).|| < r & x in (dom f) /\ A ) by A3, A2, RELAT_1:61;
hence ||.((f | A) /. x).|| < r by PARTFUN2:16; :: thesis: verum

end;

hence f | A is bounded ; :: thesis: verum