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}

hence upper_bound (rng |.seq.|) = 0 by SEQ_4:9; :: thesis: verum

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

then
rng |.seq.| = {0}
by ZFMISC_1:33;
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;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

hence upper_bound (rng |.seq.|) = 0 by SEQ_4:9; :: thesis: verum