let seq be Complex_Sequence; :: thesis: ( ( for n being Element of NAT holds seq . n = 0c ) implies ( seq is bounded & sup (rng |.seq.|) = 0 ) )
assume A1: for n being Element of NAT holds seq . n = 0c ; :: thesis: ( seq is bounded & sup (rng |.seq.|) = 0 )
for n being Element of NAT holds |.(seq . n).| < 1 by A1, COMPLEX1:130;
hence seq is bounded by COMSEQ_2:def 3; :: thesis: sup (rng |.seq.|) = 0
rng |.seq.| c= {0 }

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng |.seq.| or y in {0 } )
assume y in rng |.seq.| ; :: thesis: y in {0 }
then consider n being set such that
A2: n in NAT and
A3: |.seq.| . n = y by FUNCT_2:17;
reconsider n = n as Element of NAT by A2;
|.seq.| . n = |.(seq . n).| by VALUED_1:18
.= |.0c .| by A1 ;
hence y in {0 } by A3, COMPLEX1:130, TARSKI:def 1; :: thesis: verum

end;

then rng |.seq.| = {0 } by ZFMISC_1:39;
hence sup (rng |.seq.|) = 0 by SEQ_4:22; :: thesis: verum