theorem :: AFINSQ_1:10

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