:: deftheorem defines ^' FINSEQ_6:def 5 :
for p, q being FinSequence holds p ^' q = p ^ ((2,(len q)) -cut q);