let q, p 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 len q <> 0 ;
then 0 < len q ;
then 0 + 1 <= len q by NAT_1:13;
then 1 + 1 <= (len q) + 1 by XREAL_1:9;
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:35
.= (len p) + (len q) by A1 ; :: thesis: verum