theorem Th66: :: FINSEQ_6:66

for D being non empty set
for p being Element of D
for f1, f2 being FinSequence of D st p in rng f1 holds
(f1 ^ f2) -: p = f1 -: p