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 )
proof
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;
given r being Real such that A2: for n being Nat holds |.(s . n).| < r ; :: thesis: 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