let q, p be FinSequence; :: thesis: ( 1 < len q implies (p ^' q) . (len (p ^' q)) = q . (len q) )
set r = p ^' q;
set qc = 2,(len q) -cut q;
assume A1: 1 < len q ; :: thesis: (p ^' q) . (len (p ^' q)) = q . (len q)
then q <> {} ;
then ((len (p ^' q)) + 1) - 1 = ((len p) + (len q)) - 1 by Th13;
then A2: len (p ^' q) = (len p) + ((len q) - 1) ;
1 + 1 <= (len q) + 1 by A1, XREAL_1:9;
then (len (2,(len q) -cut q)) + (1 + 1) = (len q) + 1 by Lm2;
then A3: ((len (2,(len q) -cut q)) + 1) + 1 = (len q) + 1 ;
1 + 1 <= len q by A1, NAT_1:13;
then A4: (1 + 1) - 1 <= (len q) - 1 by XREAL_1:11;
len (2,(len q) -cut q) < len q by A3, NAT_1:13;
hence (p ^' q) . (len (p ^' q)) = q . (len q) by A2, A3, A4, Th15; :: thesis: verum