for seq being Real_Sequence st seq is bounded_above & seq is V47() holds
for n being Nat holds seq . n <= lim seq