assume F₃() <> F₄() ; :: thesis: contradiction
then consider x being set such that
A7: ( x in NAT & F₃() . x <> F₄() . x ) by A1, A4, FUNCT_1:9;
defpred S₁[ Nat] means F₃() . $1 <> F₄() . $1;
ex k being Element of NAT st S₁[k] by A7;
then A8: ex k being Nat st S₁[k] ;
consider m being Nat such that
A9: S₁[m] and
A10: for n being Nat st S₁[n] holds
m <= n from NAT_1:sch 5(A8);

now

set k = m -' 2;
assume ( m <> 0 & m <> 1 ) ; :: thesis: contradiction
then 2 <= m by NAT_1:27;
then A11: m = (m -' 2) + 2 by XREAL_1:237;
then A12: (m -' 2) + 0 < m by XREAL_1:8;
(m -' 2) + 1 < m by A11, XREAL_1:8;
then A13: F₃() . ((m -' 2) + 1) = F₄() . ((m -' 2) + 1) by A10;
( F₃() . ((m -' 2) + 2) = F₅((m -' 2),(F₃() . (m -' 2)),(F₃() . ((m -' 2) + 1))) & F₄() . ((m -' 2) + 2) = F₅((m -' 2),(F₄() . (m -' 2)),(F₄() . ((m -' 2) + 1))) ) by A3, A6;
hence contradiction by A9, A10, A11, A12, A13; :: thesis: verum

end;

hence contradiction by A2, A5, A9; :: thesis: verum