let Z be RealNormSpace; :: thesis: for A being non empty closed_interval Subset of REAL
for f being Function of A, the carrier of Z holds
( f is bounded iff is bounded )

let A be non empty closed_interval Subset of REAL; :: thesis: for f being Function of A, the carrier of Z holds
( f is bounded iff is bounded )

let f be Function of A, the carrier of Z; :: thesis: ( f is bounded iff is bounded )
hereby :: thesis: ( is bounded implies f is bounded )
assume A1: f is bounded ; :: thesis:
consider r being Real such that
A2: 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 holds
|.( . x).| < r
let x be set ; :: thesis: ( x in dom implies |.( . x).| < r )
assume A3: x in dom ; :: thesis: |.( . x).| < r
then x in dom f by NORMSP_0:def 2;
then A4: ||.(f /. x).|| < r by A2;
||.(f /. x).|| = . x by ;
hence |.( . x).| < r by ; :: thesis: verum
end;
hence ||.f.|| is bounded by COMSEQ_2:def 3; :: thesis: verum
end;
assume ||.f.|| is bounded ; :: thesis: f is bounded
then consider r being Real such that
B2: for x being set st x in dom holds
|.( . x).| < r by COMSEQ_2:def 3;
now :: thesis: for x being set st x in dom f holds
||.(f /. x).|| < r
let x be set ; :: thesis: ( x in dom f implies ||.(f /. x).|| < r )
assume x in dom f ; :: thesis: ||.(f /. x).|| < r
then B3: x in dom by NORMSP_0:def 2;
then B4: |.( . x).| < r by B2;
||.f.|| . x = ||.(f /. x).|| by ;
hence ||.(f /. x).|| < r by ; :: thesis: verum
end;
hence f is bounded ; :: thesis: verum