theorem Th71: :: AFINSQ_1:74

for p, q being XFinSequence holds p c= p ^ q