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 ;
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;
n > k by A11, NAT_1:13;
then F₃() . k = F₄() . k by A10, A12, A13;
then A14: P₁[k,F₃() . k,F₄() . (k + 1)] by A3, A12, A13;
P₁[k,F₃() . k,F₃() . (k + 1)] by A2, A12, A13;
hence contradiction by A1, A10, A11, A12, A13, A14; :: thesis: verum