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
A2: n in NAT by ORDINAL1:def 12;
0 <= abs (rseq . n) by COMPLEX1:46;
then 0 <= (abs rseq) . n by A2, SEQ_1:12;
then (abs rseq) . n = 0 by A1, A2, Lm2;
then abs (rseq . n) = 0 by A2, SEQ_1:12;
hence rseq . n = 0 by ABSVALUE:2; :: thesis: verum