F1() <> {}
by A3;
then consider r being FinSequence, a being object such that
A4:
F1() = r ^ <*a*>
by FINSEQ_1:46;
F2() <> {}
by A3;
then A5:
F1() $^ F2() = r ^ F2()
by A4, Th2;
0 + 1 <= len F2()
by A3, NAT_1:13;
then A6:
1 in Seg (len F2())
by FINSEQ_1:1;
A7:
Seg (len F2()) = dom F2()
by FINSEQ_1:def 3;
let i be Nat; ( i in dom (F1() $^ F2()) & i + 1 in dom (F1() $^ F2()) implies for x, y being set st x = (F1() $^ F2()) . i & y = (F1() $^ F2()) . (i + 1) holds
P1[x,y] )
assume that
A8:
i in dom (F1() $^ F2())
and
A9:
i + 1 in dom (F1() $^ F2())
; for x, y being set st x = (F1() $^ F2()) . i & y = (F1() $^ F2()) . (i + 1) holds
P1[x,y]
A10:
i >= 0 + 1
by A8, Lm1;
let x, y be set ; ( x = (F1() $^ F2()) . i & y = (F1() $^ F2()) . (i + 1) implies P1[x,y] )
A11:
i + 1 >= 1
by NAT_1:11;
A12: len F1() =
(len r) + (len <*a*>)
by A4, FINSEQ_1:22
.=
(len r) + 1
by FINSEQ_1:40
;
assume that
A13:
x = (F1() $^ F2()) . i
and
A14:
y = (F1() $^ F2()) . (i + 1)
; P1[x,y]
per cases
( i < len F1() or i >= len F1() )
;
suppose A15:
i < len F1()
;
P1[x,y]then
(
i in dom F1() &
i + 1
in dom F1() )
by A10, Lm3, Lm4;
then A16:
P1[
F1()
. i,
F1()
. (i + 1)]
by A1;
A17:
now ( i + 1 <= len r implies ( y = r . (i + 1) & r . (i + 1) = F1() . (i + 1) ) )end; A18:
i <= len r
by A12, A15, NAT_1:13;
then
i in Seg (len r)
by A10, FINSEQ_1:1;
then
i in dom r
by FINSEQ_1:def 3;
then A19:
(
x = r . i &
r . i = F1()
. i )
by A13, A4, A5, FINSEQ_1:def 7;
(
i = len r or
i < len r )
by A18, XXREAL_0:1;
hence
P1[
x,
y]
by A3, A6, A7, A14, A5, A12, A16, A19, A17, FINSEQ_1:def 7, NAT_1:13;
verum end; suppose
i >= len F1()
;
P1[x,y]then consider k being
Nat such that A20:
i = (len F1()) + k
by NAT_1:10;
reconsider k =
k as
Nat ;
A21:
i = (len r) + (1 + k)
by A12, A20;
len (F1() $^ F2()) = (len r) + (len F2())
by A5, FINSEQ_1:22;
then A22:
k + 1
< len F2()
by A9, A21, Lm2, XREAL_1:7;
then A23:
(k + 1) + 1
in dom F2()
by Lm4;
A24:
k + 1
in dom F2()
by A22, Lm3;
then A25:
x = F2()
. (k + 1)
by A13, A5, A21, FINSEQ_1:def 7;
((len r) + (1 + k)) + 1
= (len r) + ((k + 1) + 1)
;
then
y = F2()
. ((k + 1) + 1)
by A14, A5, A12, A20, A23, FINSEQ_1:def 7;
hence
P1[
x,
y]
by A2, A24, A23, A25;
verum end;