theorem Th1: :: LOPBAN_5:1

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