for seq being Real_Sequence
for r being Real st seq is bounded & 0 <= r holds
lim_sup (r (#) seq) = r * (lim_sup seq)