1 in NAT ;
then reconsider j = 1 as Element of REAL by NUMBERS:19;
take sc ; :: thesis: sc is bounded
take j ; :: according to COMSEQ_2:def 4 :: thesis: for n being Nat holds |.(sc . n).| < j
let n be Nat; :: thesis: |.(sc . n).| < j
n in NAT by ORDINAL1:def 12;
hence |.(sc . n).| < j by COMPLEX1:44, FUNCOP_1:7; :: thesis: verum