for r being Real
for seq1, seq2 being Real_Sequence holds
( seq1 = r (#) seq2 iff for n being Nat holds seq1 . n = r * (seq2 . n) )