theorem :: VALUED_1:49

for p1, p2 being FinSequence holds p1 ^ p2 = p1 \/ (Shift (p2,(len p1)))