theorem Th12: :: AFINSQ_2:12
for p, q being XFinSequence holds (p ^ q) /^ (len p) = q