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 )

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;

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

end;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

hence
||.f.|| is bounded
by COMSEQ_2:def 3; :: thesis: verum|.(||.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;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

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

hence
f is bounded
; :: thesis: verum||.(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;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