for seq being Real_Sequence
for r being Real holds
( ( seq is divergent_to+infty & r > 0 implies r (#) seq is divergent_to+infty ) & ( seq is divergent_to+infty & r < 0 implies r (#) seq is divergent_to-infty ) & ( r = 0 implies ( rng (r (#) seq) = {0} & r (#) seq is constant ) ) )