theorem :: AFINSQ_2:19
for p, q being XFinSequence holds mid ((p ^ q),((len p) + 1),((len p) + (len q))) = q