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