defpred S1[ object ] means F5() . $1 <> F6() . $1;
consider X being set such that
A9:
for Y being object holds
( Y in X iff ( Y in F1() & S1[Y] ) )
from XBOOLE_0:sch 1();
for b being object st b in X holds
b in F1()
by A9;
then A10:
X c= F1()
;
assume
F5() <> F6()
; contradiction
then
ex a being object st
( a in F1() & F5() . a <> F6() . a )
by A1, A5, FUNCT_1:2;
then
X <> 0
by A9;
then consider B being Ordinal such that
A11:
B in X
and
A12:
for C being Ordinal st C in X holds
B c= C
by A10, ORDINAL1:20;
A13:
B in F1()
by A9, A11;
then A14:
B c= F1()
by ORDINAL1:def 2;
then A15:
( dom (F5() | B) = B & dom (F6() | B) = B )
by A1, A5, RELAT_1:62;
A20:
now ( ex C being Ordinal st B = succ C implies F5() . B = F6() . B )given C being
Ordinal such that A21:
B = succ C
;
F5() . B = F6() . BA22:
(
F5()
. C = (F5() | B) . C &
F6()
. C = (F6() | B) . C )
by A21, FUNCT_1:49, ORDINAL1:6;
(
F5()
. B = F3(
C,
(F5() . C)) &
F6()
. B = F3(
C,
(F6() . C)) )
by A3, A7, A13, A21;
hence
F5()
. B = F6()
. B
by A18, A21, A22, ORDINAL1:6;
verum end;
hence
contradiction
by A2, A6, A9, A11, A20; verum