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; :: thesis: ( 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()) ; :: thesis: 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 ; :: thesis: ( 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) ; :: thesis: P1[x,y]
per cases ( i < len F1() or i >= len F1() ) ;
suppose A15: i < len F1() ; :: thesis: 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 :: thesis: ( i + 1 <= len r implies ( y = r . (i + 1) & r . (i + 1) = F1() . (i + 1) ) )
assume i + 1 <= len r ; :: thesis: ( y = r . (i + 1) & r . (i + 1) = F1() . (i + 1) )
then i + 1 in Seg (len r) by A11, FINSEQ_1:1;
then i + 1 in dom r by FINSEQ_1:def 3;
hence ( y = r . (i + 1) & r . (i + 1) = F1() . (i + 1) ) by A14, A4, A5, FINSEQ_1:def 7; :: thesis: verum
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; :: thesis: verum
end;
suppose i >= len F1() ; :: thesis: 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; :: thesis: verum
end;
end;