let f, g be FinSequence; :: thesis: len f <= len (f ^' g)
f ^' g = f ^ (2,(len g) -cut g) by GRAPH_2:def 2;
then len (f ^' g) = (len f) + (len (2,(len g) -cut g)) by FINSEQ_1:35;
hence len f <= len (f ^' g) by NAT_1:11; :: thesis: verum