for seq being ExtREAL_sequence
for r being Real st ( for n being Nat holds seq . n = r ) holds
( seq is convergent_to_finite_number & lim seq = r )