defpred S1[ Nat] means F5() . $1 <> F6() . $1;
assume
F5() <> F6()
; 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 not m <> 0 & ... & m <> 3set 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
;
contradictionthen
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;
verum end;
hence
contradiction
by A2, A5, A8; verum