theorem Th78: :: AFINSQ_2:79

for p, q being XFinSequence st p c= q holds
ex r being XFinSequence st p ^ r = q