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

now

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

end;

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