seq_id Zeroseq is bounded

proof

reconsider rseq = seq_id Zeroseq as Real_Sequence ;
for n being Nat holds rseq . n = 0

proof

let n be Nat; :: thesis: rseq . n = 0
n in NAT by ORDINAL1:def 13;
hence rseq . n = 0 by RSSPACE:def 6; :: thesis: verum

end;

then rseq is constant by VALUED_0:def 18;
hence seq_id Zeroseq is bounded ; :: thesis: verum

end;

hence not the_set_of_BoundedRealSequences is empty by Def1; :: thesis: verum