theorem :: FINSEQ_2:39

for i being natural Number
for p being FinSequence
for f being Function of (Seg i),(Seg i) st i <= len p holds
p * f is FinSequence by Th36;