let seq be Complex_Sequence; :: thesis: ( ( for n being Nat holds seq . n = 0c ) implies ( seq is bounded & upper_bound (rng |.seq.|) = 0 ) )
assume A1: for n being Nat holds seq . n = 0c ; :: thesis: ( seq is bounded & upper_bound (rng |.seq.|) = 0 )
for n being Nat holds |.(seq . n).| < jj by A1, COMPLEX1:44;
hence seq is bounded by COMSEQ_2:def 4; :: thesis: upper_bound (rng |.seq.|) = 0
rng |.seq.| c= {0}
proof
let y be object ; :: 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 object such that
A2: n in NAT and
A3: |.seq.| . n = y by FUNCT_2:11;
reconsider n = n as Nat by A2;
|.seq.| . n = |.(seq . n).| by VALUED_1:18
.= |.0c.| by A1 ;
hence y in {0} by A3, COMPLEX1:44, TARSKI:def 1; :: thesis: verum
end;
then rng |.seq.| = {0} by ZFMISC_1:33;
hence upper_bound (rng |.seq.|) = 0 by SEQ_4:9; :: thesis: verum