thus ( s is bounded implies ex r being Real st
for n being Element of NAT holds |.(s . n).| < r ) :: thesis: ( ex r being Real st
for n being Element of NAT holds |.(s . n).| < r implies s is bounded )

proof

given r being real number such that A1: for y being set st y in dom s holds
abs (s . y) < r ; :: according to SEQ_2:def 5 :: thesis: ex r being Real st
for n being Element of NAT holds |.(s . n).| < r
reconsider r = r as Element of REAL by XREAL_0:def 1;
take r ; :: thesis: for n being Element of NAT holds |.(s . n).| < r
let n be Element of NAT ; :: thesis: |.(s . n).| < r
n in NAT ;
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 Element of NAT holds |.(s . n).| < r ; :: thesis: s is bounded
take r ; :: according to SEQ_2:def 5 :: thesis: for b₁ being set holds
( not b₁ in K1(s) or not r <= abs (s . b₁) )
let y be set ; :: thesis: ( not y in K1(s) or not r <= abs (s . y) )
assume y in dom s ; :: thesis: not r <= abs (s . y)
hence not r <= abs (s . y) by A2; :: thesis: verum