let p, q 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 1 + 1 <= len q by NAT_1:13;
then A2: (1 + 1) - 1 <= (len q) - 1 by XREAL_1:9;
q <> {} by A1;
then ((len (p ^' q)) + 1) - 1 = ((len p) + (len q)) - 1 by Th13;
then A3: len (p ^' q) = (len p) + ((len q) - 1) ;
1 + 1 <= (len q) + 1 by A1, XREAL_1:7;
then (len ((2,(len q)) -cut q)) + (1 + 1) = (len q) + 1 by Lm2;
then A4: ((len ((2,(len q)) -cut q)) + 1) + 1 = (len q) + 1 ;
then len ((2,(len q)) -cut q) < len q by NAT_1:13;
hence (p ^' q) . (len (p ^' q)) = q . (len q) by A3, A4, A2, Th15; :: thesis: verum