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