let rseq be Real_Sequence; :: thesis: ( ( for n being Nat holds rseq . n = 0 ) implies ( rseq is bounded & sup (rng (abs rseq)) = 0 ) )
assume A1: for n being Nat holds rseq . n = 0 ; :: thesis: ( rseq is bounded & sup (rng (abs rseq)) = 0 )
A2: for n being Nat holds (abs rseq) . n = 0

proof

let n be Nat; :: thesis: (abs rseq) . n = 0
X: n in NAT by ORDINAL1:def 13;
A3: rseq . n = 0 by A1;
(abs rseq) . n = abs (rseq . n) by X, SEQ_1:16;
hence (abs rseq) . n = 0 by A3, ABSVALUE:7; :: thesis: verum

end;

A4: rseq is constant by A1, VALUED_0:def 18;
rng (abs rseq) = {0 }

proof

rng (abs rseq) c= {0 }

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (abs rseq) or y in {0 } )
assume y in rng (abs rseq) ; :: thesis: y in {0 }
then consider n being set such that
A5: ( n in NAT & (abs rseq) . n = y ) by FUNCT_2:17;
y = 0 by A2, A5;
hence y in {0 } by TARSKI:def 1; :: thesis: verum

end;

hence rng (abs rseq) = {0 } by ZFMISC_1:39; :: thesis: verum

end;

hence ( rseq is bounded & sup (rng (abs rseq)) = 0 ) by A4, SEQ_4:22; :: thesis: verum