let q, p be FinSequence; :: thesis: 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 ; :: 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)then
len q <> 0
;
then
0 < len q
;
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;
then A5:
k in dom (2,(len q) -cut q)
by A1, FINSEQ_3:27;
0 + 1
<= k
by A1;
then consider i being
Element of
NAT such that A6:
(
0 <= i &
i < len (2,(len q) -cut q) &
k = i + 1 )
by A4, Th1;
thus (p ^' q) . ((len p) + k) =
(2,(len q) -cut q) . k
by A5, FINSEQ_1:def 7
.=
q . ((1 + 1) + i)
by A3, A6, Lm2
.=
q . (k + 1)
by A6
;
:: thesis: verum end;