defpred S₁[ Nat] means ( 1 <= $1 & $1 <= F₃() & F₄() . $1 <> F₅() . $1 );
assume A4: F₄() <> F₅() ; :: thesis: contradiction
dom F₄() = Seg (len F₅()) by A2, A3, FINSEQ_1:def 3
.= dom F₅() by FINSEQ_1:def 3 ;
then consider x being object such that
A5: x in dom F₄() and
A6: F₄() . x <> F₅() . x by A4;
A7: x in Seg (len F₄()) by A5, FINSEQ_1:def 3;
reconsider x = x as Nat by A5;
A8: 1 <= x by A7, FINSEQ_1:1;
x <= F₃() by A2, A7, FINSEQ_1:1;
then A9: ex n being Nat st S₁[n] by A6, A8;
consider n being Nat such that
A10: ( S₁[n] & ( for k being Nat st S₁[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 = F₅() . (k + 1) as Element of F₁() 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 < F₃() by A10, XXREAL_0:2;
then reconsider Fk = F₄() . k as Element of F₁() by A2, A12, Lm1;
n > k by A11, NAT_1:13;
then F₄() . k = F₅() . k by A10, A12, A13;
then A14: P₁[k,Fk,Gk1] by A3, A12, A13;
reconsider Fk1 = F₄() . (k + 1) as Element of F₁() by A2, A10, A11, Lm1;
P₁[k,Fk,Fk1] by A2, A12, A13;
hence contradiction by A1, A10, A11, A12, A13, A14; :: thesis: verum