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

proof

let n be Nat; :: thesis: (abs rseq) . n = 0
A3: (abs rseq) . n = |.(rseq . n).| by SEQ_1:12;
rseq . n = 0 by A1;
hence (abs rseq) . n = 0 by A3, ABSVALUE:2; :: thesis: verum

end;

rng (abs rseq) c= {0}

proof

let y be object ; :: 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 ex n being object st
( n in NAT & (abs rseq) . n = y ) by FUNCT_2:11;
then y = 0 by A2;
hence y in {0} by TARSKI:def 1; :: thesis: verum

end;

then A4: rng (abs rseq) = {0} by ZFMISC_1:33;
rseq is constant by A1, VALUED_0:def 18;
hence ( rseq is bounded & upper_bound (rng (abs rseq)) = 0 ) by A4, SEQ_4:9; :: thesis: verum