theorem :: RFINSEQ:25

for R being FinSequence of REAL holds (0 * R) " {0} = dom R