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 -' 4;
assume ( m <> 0 & m <> 1 & m <> 2 & m <> 3 ) ; :: thesis: contradiction
then 4 <= m by NAT_1:29;
then A11: m = (m -' 4) + 4 by XREAL_1:237;
then A12: (m -' 4) + 0 < m by XREAL_1:8;
(m -' 4) + 1 < m by A11, XREAL_1:8;
then A13: F₅() . ((m -' 4) + 1) = F₆() . ((m -' 4) + 1) by A10;
(m -' 4) + 2 < m by A11, XREAL_1:8;
then A14: F₅() . ((m -' 4) + 2) = F₆() . ((m -' 4) + 2) by A10;
(m -' 4) + 3 < m by A11, XREAL_1:8;
then A15: F₅() . ((m -' 4) + 3) = F₆() . ((m -' 4) + 3) by A10;
( F₅() . ((m -' 4) + 4) = F₇((m -' 4),(F₅() . (m -' 4)),(F₅() . ((m -' 4) + 1)),(F₅() . ((m -' 4) + 2)),(F₅() . ((m -' 4) + 3))) & F₆() . ((m -' 4) + 4) = F₇((m -' 4),(F₆() . (m -' 4)),(F₆() . ((m -' 4) + 1)),(F₆() . ((m -' 4) + 2)),(F₆() . ((m -' 4) + 3))) ) by A3, A6;
hence contradiction by A9, A10, A11, A12, A13, A14, A15; :: thesis: verum

end;

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