assume A4: F₄() <> F₅() ; :: thesis: contradiction
dom F₄() = dom F₅() by A2, A3, FINSEQ_3:31;
then consider x being set such that
A5: x in dom F₄() and
A6: F₄() . x <> F₅() . x by A4, FUNCT_1:9;
A7: x in Seg (len F₄()) by A5, FINSEQ_1:def 3;
dom F₄() = Seg F₃() by A2, FINSEQ_1:def 3
.= dom F₅() by A3, FINSEQ_1:def 3 ;
then A8: F₅() /. x = F₅() . x by A5, PARTFUN1:def 8;
defpred S₁[ Nat] means ( 1 <= $1 & $1 <= F₃() & F₄() /. $1 <> F₅() /. $1 );
A9: F₄() /. x = F₄() . x by A5, PARTFUN1:def 8;
reconsider x = x as Element of NAT by A5;
A10: 1 <= x by A7, FINSEQ_1:3;
x <= F₃() by A2, A7, FINSEQ_1:3;
then A11: ex n being Nat st S₁[n] by A6, A9, A8, A10;
consider n being Nat such that
A12: ( S₁[n] & ( for k being Nat st S₁[k] holds
n <= k ) ) from NAT_1:sch 5(A11);
consider k being Nat such that
A13: n = k + 1 by A12, NAT_1:6;
n <> 1 by A2, A3, A12;
then 1 < n by A12, XXREAL_0:1;
then A14: 1 <= k by A13, NAT_1:13;
k <= n by A13, NAT_1:11;
then A15: k <= F₃() by A12, XXREAL_0:2;
reconsider Fk = F₄() /. k, Fk1 = F₄() /. (k + 1), Gk1 = F₅() /. (k + 1) as Element of F₁() ;
A16: k in NAT by ORDINAL1:def 13;
A17: k <= F₃() - 1 by A12, A13, XREAL_1:21;
then A18: P₁[k,Fk,Fk1] by A2, A14, A16;
n > k by A13, NAT_1:13;
then F₄() /. k = F₅() /. k by A12, A14, A15;
then P₁[k,Fk,Gk1] by A3, A14, A16, A17;
hence contradiction by A1, A12, A13, A14, A16, A17, A18; :: thesis: verum