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