p ^' q = p ^ ((2,(len q)) -cut q) by FINSEQ_6:def 5;
hence p ^' q is Cycle-like ; :: thesis: verum