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 ||.f.|| 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 ||.f.|| is bounded )
let f be Function of A, the carrier of Z; :: thesis: ( f is bounded iff ||.f.|| is bounded )

hereby :: thesis: ( ||.f.|| is bounded implies f is bounded )

assume A1: f is bounded ; :: thesis: ||.f.|| is bounded
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 ||.f.|| holds
|.(||.f.|| . x).| < r

let x be set ; :: thesis: ( x in dom ||.f.|| implies |.(||.f.|| . x).| < r )
assume A3: x in dom ||.f.|| ; :: thesis: |.(||.f.|| . x).| < r
then x in dom f by NORMSP_0:def 2;
then A4: ||.(f /. x).|| < r by A2;
||.(f /. x).|| = ||.f.|| . x by A3, NORMSP_0:def 2;
hence |.(||.f.|| . x).| < r by A4, ABSVALUE:def 1; :: 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 ||.f.|| holds
|.(||.f.|| . 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 ||.f.|| by NORMSP_0:def 2;
then B4: |.(||.f.|| . x).| < r by B2;
||.f.|| . x = ||.(f /. x).|| by B3, NORMSP_0:def 2;
hence ||.(f /. x).|| < r by B4, ABSVALUE:def 1; :: thesis: verum

end;

hence f is bounded ; :: thesis: verum