defpred S_{1}[ Nat] means F_{4}() . $1 <> F_{5}() . $1;

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

then ex x being object st

( x in NAT & F_{4}() . x <> F_{5}() . x )
by A1, A4, FUNCT_1:2;

then A7: ex k being Nat st S_{1}[k]
;

consider m being Nat such that

A8: S_{1}[m]
and

A9: for n being Nat st S_{1}[n] holds

m <= n from NAT_1:sch 5(A7);

assume F

then ex x being object st

( x in NAT & F

then A7: ex k being Nat st S

consider m being Nat such that

A8: S

A9: for n being Nat st S

m <= n from NAT_1:sch 5(A7);

now :: thesis: not m <> 0 & ... & m <> 2

hence
contradiction
by A2, A5, A8; :: thesis: verumset k = m -' 3;

A10: ( F_{4}() . ((m -' 3) + 3) = F_{6}((m -' 3),(F_{4}() . (m -' 3)),(F_{4}() . ((m -' 3) + 1)),(F_{4}() . ((m -' 3) + 2))) & F_{5}() . ((m -' 3) + 3) = F_{6}((m -' 3),(F_{5}() . (m -' 3)),(F_{5}() . ((m -' 3) + 1)),(F_{5}() . ((m -' 3) + 2))) )
by A3, A6;

assume m <> 0 & ... & m <> 2 ; :: thesis: contradiction

then 2 < m ;

then 2 + 1 <= m by NAT_1:13;

then A11: m = (m -' 3) + 3 by XREAL_1:235;

then A12: F_{4}() . ((m -' 3) + 1) = F_{5}() . ((m -' 3) + 1)
by A9, XREAL_1:6;

A13: F_{4}() . ((m -' 3) + 2) = F_{5}() . ((m -' 3) + 2)
by A9, A11, XREAL_1:6;

(m -' 3) + 0 < m by A11, XREAL_1:6;

hence contradiction by A8, A9, A11, A12, A13, A10; :: thesis: verum

end;A10: ( F

assume m <> 0 & ... & m <> 2 ; :: thesis: contradiction

then 2 < m ;

then 2 + 1 <= m by NAT_1:13;

then A11: m = (m -' 3) + 3 by XREAL_1:235;

then A12: F

A13: F

(m -' 3) + 0 < m by A11, XREAL_1:6;

hence contradiction by A8, A9, A11, A12, A13, A10; :: thesis: verum