theorem Th12: :: AFINSQ_2:12

for p, q being XFinSequence holds (p ^ q) /^ (len p) = q