theorem Th74: :: AFINSQ_1:77

for p, q being XFinSequence holds p ^ q = p +* (Shift (q,(card p)))