let f, g be FinSequence; :: thesis: rng f c= rng (f ^' g)
f ^' g = f ^ ((2,(len g)) -cut g) by GRAPH_2:def 2;
hence rng f c= rng (f ^' g) by FINSEQ_1:29; :: thesis: verum