defpred S_{1}[ Nat] means ( 1 <= $1 & $1 <= F_{2}() & F_{3}() . $1 <> F_{4}() . $1 );

assume A4: F_{3}() <> F_{4}()
; :: thesis: contradiction

dom F_{3}() =
Seg (len F_{4}())
by A2, A3, FINSEQ_1:def 3

.= dom F_{4}()
by FINSEQ_1:def 3
;

then consider x being object such that

A5: x in dom F_{3}()
and

A6: F_{3}() . x <> F_{4}() . x
by A4;

A7: x in Seg (len F_{3}())
by A5, FINSEQ_1:def 3;

reconsider x = x as Nat by A5;

A8: 1 <= x by A7, FINSEQ_1:1;

x <= F_{2}()
by A2, A7, FINSEQ_1:1;

then A9: ex n being Nat st S_{1}[n]
by A6, A8;

consider n being Nat such that

A10: ( S_{1}[n] & ( for k being Nat st S_{1}[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_{2}()
by A10, XXREAL_0:2;

n > k by A11, NAT_1:13;

then F_{3}() . k = F_{4}() . k
by A10, A12, A13;

then A14: P_{1}[k,F_{3}() . k,F_{4}() . (k + 1)]
by A3, A12, A13;

P_{1}[k,F_{3}() . k,F_{3}() . (k + 1)]
by A2, A12, A13;

hence contradiction by A1, A10, A11, A12, A13, A14; :: thesis: verum

assume A4: F

dom F

.= dom F

then consider x being object such that

A5: x in dom F

A6: F

A7: x in Seg (len F

reconsider x = x as Nat by A5;

A8: 1 <= x by A7, FINSEQ_1:1;

x <= F

then A9: ex n being Nat st S

consider n being Nat such that

A10: ( S

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

n > k by A11, NAT_1:13;

then F

then A14: P

P

hence contradiction by A1, A10, A11, A12, A13, A14; :: thesis: verum