for R being FinSequence of REAL
for r, s being Real st r <> 0 holds
R " {(s / r)} = (r * R) " {s}