for L, K being ExtREAL_sequence
for c being Real st 0 <= c & L is () & ( for n being Nat holds K . n = c * (L . n) ) holds
( sup (rng K) = c * (sup (rng L)) & K is () )