theorem Th62: :: FINSEQ_2:64

for p, q being FinSequence
for F being Function st [:(rng p),(rng q):] c= dom F holds
F .: (p,q) is FinSequence