theorem Th68: :: FINSEQ_2:70

for D, D9, E being non empty set
for F being Function of [:D,D9:],E
for p being FinSequence of D
for q being FinSequence of D9 holds F .: (p,q) is FinSequence of E