for rseq being Real_Sequence holds
( ( rseq is bounded & upper_bound (rng (abs rseq)) = 0 ) iff for n being Nat holds rseq . n = 0 ) by Lm5, Lm6;