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