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