f ^' g = f ^ ((2,(len g)) -cut g) by FINSEQ_6:def 5;
hence not f ^' g is empty ; :: thesis: verum