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 ;
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 ;
k in dom ((2,(len q)) -cut q) by ;
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;