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