defpred S1[ Nat] means F5() . $1 <> F6() . $1;
assume F5() <> F6() ; :: thesis: contradiction
then ex x being object st
( x in NAT & F5() . x <> F6() . x ) by A1, A4, FUNCT_1:2;
then A7: ex k being Nat st S1[k] ;
consider m being Nat such that
A8: S1[m] and
A9: for n being Nat st S1[n] holds
m <= n from NAT_1:sch 5(A7);
now :: thesis: not m <> 0 & ... & m <> 3
set k = m -' 4;
A10: ( F5() . ((m -' 4) + 4) = F7((m -' 4),(F5() . (m -' 4)),(F5() . ((m -' 4) + 1)),(F5() . ((m -' 4) + 2)),(F5() . ((m -' 4) + 3))) & F6() . ((m -' 4) + 4) = F7((m -' 4),(F6() . (m -' 4)),(F6() . ((m -' 4) + 1)),(F6() . ((m -' 4) + 2)),(F6() . ((m -' 4) + 3))) ) by A3, A6;
assume m <> 0 & ... & m <> 3 ; :: thesis: contradiction
then 3 < m ;
then 3 + 1 <= m by NAT_1:13;
then A11: m = (m -' 4) + 4 by XREAL_1:235;
then A12: F5() . ((m -' 4) + 1) = F6() . ((m -' 4) + 1) by A9, XREAL_1:6;
(m -' 4) + 3 < m by A11, XREAL_1:6;
then A13: F5() . ((m -' 4) + 3) = F6() . ((m -' 4) + 3) by A9;
(m -' 4) + 2 < m by A11, XREAL_1:6;
then A14: F5() . ((m -' 4) + 2) = F6() . ((m -' 4) + 2) by A9;
(m -' 4) + 0 < m by A11, XREAL_1:6;
hence contradiction by A8, A9, A11, A12, A14, A13, A10; :: thesis: verum
end;
hence contradiction by A2, A5, A8; :: thesis: verum