theorem :: FINSEQ_1:16

for f being Function
for p being FinSequence st rng p c= dom f holds
f * p is FinSequence