theorem Th77: :: AFINSQ_2:78

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