let rseq be Real_Sequence; :: thesis: ( rseq is bounded & sup (rng (abs rseq)) = 0 implies for n being Nat holds rseq . n = 0 )
assume that
A1: rseq is bounded and
A2: sup (rng (abs rseq)) = 0 ; :: thesis: for n being Nat holds rseq . n = 0
let n be Nat; :: thesis: rseq . n = 0
X: n in NAT by ORDINAL1:def 13;
A3: abs rseq is bounded by A1;
0 <= (abs rseq) . n

proof

0 <= abs (rseq . n) by COMPLEX1:132;
hence 0 <= (abs rseq) . n by X, SEQ_1:16; :: thesis: verum

end;

then (abs rseq) . n = 0 by A2, A3, Lm2, X;
then abs (rseq . n) = 0 by X, SEQ_1:16;
hence rseq . n = 0 by ABSVALUE:7; :: thesis: verum