theorem :: RFINSEQ:25

for R being real-valued FinSequence holds (0 * R) " {0} = dom R