for i, j being natural Number
for p being FinSequence
for f being Function of (Seg i),(Seg j) st ( j = 0 implies i = 0 ) & j <= len p holds
p * f is FinSequence