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:42; :: thesis: verum