let q, p be FinSequence; for k being Element of NAT st 1 <= k & k < len q holds
(p ^' q) . ((len p) + k) = q . (k + 1)
let k be Element of 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:9;
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
Element of
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:27;
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;