let rseq be Real_Sequence; :: thesis: ( rseq is bounded & upper_bound (rng (abs rseq)) = 0 implies for n being Nat holds rseq . n = 0 )
assume A1: ( rseq is bounded & upper_bound (rng (abs rseq)) = 0 ) ; :: thesis: for n being Nat holds rseq . n = 0
let n be Nat; :: thesis: rseq . n = 0
0 <= |.(rseq . n).| by COMPLEX1:46;
then 0 <= (abs rseq) . n by SEQ_1:12;
then (abs rseq) . n = 0 by A1, Lm2;
then |.(rseq . n).| = 0 by SEQ_1:12;
hence rseq . n = 0 by ABSVALUE:2; :: thesis: verum