let p, q be FinSequence; :: thesis: for k being Nat st 1 <= k & k < len q holds
(p ^' q) . ((len p) + k) = q . (k + 1)
let k be Nat; :: thesis: ( 1 <= k & k < len q implies (p ^' q) . ((len p) + k) = q . (k + 1) )
set qc = (2,(len q)) -cut q;
assume that
A1: 1 <= k and
A2: k < len q ; :: thesis: (p ^' q) . ((len p) + k) = q . (k + 1)

per cases ( q = {} or q <> {} ) ;

suppose q = {} ; :: thesis: (p ^' q) . ((len p) + k) = q . (k + 1)

hence (p ^' q) . ((len p) + k) = q . (k + 1) by A2; :: thesis: verum

end;

suppose q <> {} ; :: thesis: (p ^' q) . ((len p) + k) = q . (k + 1)

then 0 + 1 <= len q by NAT_1:13;
then A3: 1 + 1 <= (len q) + 1 by XREAL_1:7;
then (len ((2,(len q)) -cut q)) + (1 + 1) = (len q) + 1 by Lm2;
then ((len ((2,(len q)) -cut q)) + 1) + 1 = (len q) + 1 ;
then A4: k <= len ((2,(len q)) -cut q) by A2, NAT_1:13;
0 + 1 <= k by A1;
then consider i being Nat such that
0 <= i and
A5: i < len ((2,(len q)) -cut q) and
A6: k = i + 1 by A4, Th1;
k in dom ((2,(len q)) -cut q) by A1, A4, FINSEQ_3:25;
hence (p ^' q) . ((len p) + k) = ((2,(len q)) -cut q) . k by FINSEQ_1:def 7
.= q . ((1 + 1) + i) by A3, A5, A6, Lm2
.= q . (k + 1) by A6 ;
:: thesis: verum

end;

end;