defpred S1[ Nat] means ( 1 <= $1 & $1 <= F3() & F4() . $1 <> F5() . $1 );
assume A4:
F4() <> F5()
; contradiction
dom F4() =
Seg (len F5())
by A2, A3, FINSEQ_1:def 3
.=
dom F5()
by FINSEQ_1:def 3
;
then consider x being object such that
A5:
x in dom F4()
and
A6:
F4() . x <> F5() . x
by A4;
A7:
x in Seg (len F4())
by A5, FINSEQ_1:def 3;
reconsider x = x as Nat by A5;
A8:
1 <= x
by A7, FINSEQ_1:1;
x <= F3()
by A2, A7, FINSEQ_1:1;
then A9:
ex n being Nat st S1[n]
by A6, A8;
consider n being Nat such that
A10:
( S1[n] & ( for k being Nat st S1[k] holds
n <= k ) )
from NAT_1:sch 5(A9);
0 <> n
by A10;
then consider k being Nat such that
A11:
n = k + 1
by NAT_1:6;
reconsider k = k as Nat ;
reconsider Gk1 = F5() . (k + 1) as Element of F1() by A3, A10, A11, Lm1;
n <> 1
by A2, A3, A10;
then
1 < n
by A10, XXREAL_0:1;
then A12:
1 <= k
by A11, NAT_1:13;
k < n
by A11, XREAL_1:29;
then A13:
k < F3()
by A10, XXREAL_0:2;
then reconsider Fk = F4() . k as Element of F1() by A2, A12, Lm1;
n > k
by A11, NAT_1:13;
then
F4() . k = F5() . k
by A10, A12, A13;
then A14:
P1[k,Fk,Gk1]
by A3, A12, A13;
reconsider Fk1 = F4() . (k + 1) as Element of F1() by A2, A10, A11, Lm1;
P1[k,Fk,Fk1]
by A2, A12, A13;
hence
contradiction
by A1, A10, A11, A12, A13, A14; verum