thus
( s is bounded implies ex r being Real st

for n being Nat holds |.(s . n).| < r ) :: thesis: ( ex r being Real st

for n being Nat holds |.(s . n).| < r implies s is bounded )

take r ; :: according to COMSEQ_2:def 3 :: thesis: for y being set st y in dom s holds

|.(s . y).| < r

let y be set ; :: thesis: ( y in dom s implies |.(s . y).| < r )

assume y in dom s ; :: thesis: |.(s . y).| < r

hence |.(s . y).| < r by A2; :: thesis: verum

for n being Nat holds |.(s . n).| < r ) :: thesis: ( ex r being Real st

for n being Nat holds |.(s . n).| < r implies s is bounded )

proof

given r being Real such that A2:
for n being Nat holds |.(s . n).| < r
; :: thesis: s is bounded
given r being Real such that A1:
for y being set st y in dom s holds

|.(s . y).| < r ; :: according to COMSEQ_2:def 3 :: thesis: ex r being Real st

for n being Nat holds |.(s . n).| < r

reconsider r = r as Element of REAL by XREAL_0:def 1;

take r ; :: thesis: for n being Nat holds |.(s . n).| < r

let n be Nat; :: thesis: |.(s . n).| < r

n in NAT by ORDINAL1:def 12;

then n in dom s by FUNCT_2:def 1;

hence |.(s . n).| < r by A1; :: thesis: verum

end;|.(s . y).| < r ; :: according to COMSEQ_2:def 3 :: thesis: ex r being Real st

for n being Nat holds |.(s . n).| < r

reconsider r = r as Element of REAL by XREAL_0:def 1;

take r ; :: thesis: for n being Nat holds |.(s . n).| < r

let n be Nat; :: thesis: |.(s . n).| < r

n in NAT by ORDINAL1:def 12;

then n in dom s by FUNCT_2:def 1;

hence |.(s . n).| < r by A1; :: thesis: verum

take r ; :: according to COMSEQ_2:def 3 :: thesis: for y being set st y in dom s holds

|.(s . y).| < r

let y be set ; :: thesis: ( y in dom s implies |.(s . y).| < r )

assume y in dom s ; :: thesis: |.(s . y).| < r

hence |.(s . y).| < r by A2; :: thesis: verum