let p, q be FinSequence; :: thesis: ( q <> {} implies (len (p ^' q)) + 1 = (len p) + (len q) )
set r = p ^' q;
set qc = (2,(len q)) -cut q;
assume q <> {} ; :: thesis: (len (p ^' q)) + 1 = (len p) + (len q)
then 0 + 1 <= len q by NAT_1:13;
then 1 + 1 <= (len q) + 1 by XREAL_1:7;
then A1: (len ((2,(len q)) -cut q)) + (1 + 1) = (len q) + 1 by Lm2;
thus (len (p ^' q)) + 1 = ((len p) + (len ((2,(len q)) -cut q))) + 1 by FINSEQ_1:22
.= (len p) + (len q) by A1 ; :: thesis: verum