for seq being Real_Sequence st ( for n being Nat holds seq . n = n ) holds
seq is divergent_to+infty