let Z be RealNormSpace; :: thesis:
let A be non empty closed_interval Subset of REAL; :: thesis:
let f be Function of A, the carrier of Z; :: thesis:

hereby :: thesis:

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;

let x be set ; :: thesis:
assume A3: x in dom ||.f.|| ; :: thesis:
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:

end;

hence ||.f.|| is bounded by COMSEQ_2:def 3; :: thesis:

end;

assume ||.f.|| is bounded ; :: thesis:
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;

let x be set ; :: thesis:
assume x in dom f ; :: thesis:
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:

end;

hence f is bounded ; :: thesis: