theorem :: AFINSQ_1:41

for p, q, r, s being XFinSequence st p ^ q = r ^ s & len p <= len r holds
ex t being XFinSequence st p ^ t = r