theorem :: RFINSEQ:24

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