theorem Th4: :: RINFSUP1:4

for seq being Real_Sequence holds rng (- seq) = -- (rng seq)