let p, q be FinSequence; for k being Nat st 1 <= k & k < len q holds
(p ^' q) . ((len p) + k) = q . (k + 1)
let k be Nat; ( 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
; (p ^' q) . ((len p) + k) = q . (k + 1)
per cases
( q = {} or q <> {} )
;
suppose
q <> {}
;
(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
;
verum end;