theorem Th9: :: NAT_5:9

for X being set
for f1 being FinSequence of NAT
for f2 being FinSequence of X st rng f1 c= dom f2 holds
f2 * f1 is FinSequence of X