defpred S₁[ object ] means F₃() . $1 <> F₄() . $1;
consider X being set such that
A3: for x being object holds
( x in X iff ( x in F₁() & S₁[x] ) ) from XBOOLE_0:sch 1();
for b being object st b in X holds
b in F₁() by A3;
then A4: X c= F₁() ;
assume F₃() <> F₄() ; :: thesis: contradiction
then ex a being object st
( a in F₁() & F₃() . a <> F₄() . a ) by A1, A2;
then X <> {} by A3;
then consider B being Ordinal such that
A5: B in X and
A6: for C being Ordinal st C in X holds
B c= C by A4, Th16;
A7: B in F₁() by A3, A5;
then A8: B c= F₁() by Def2;
then A9: dom (F₃() | B) = B by A1, RELAT_1:62;
A10: dom (F₄() | B) = B by A2, A8, RELAT_1:62;

A11: now :: thesis: for C being Ordinal st C in B holds
F₃() . C = F₄() . C

let C be Ordinal; :: thesis: ( C in B implies F₃() . C = F₄() . C )
assume A12: C in B ; :: thesis: F₃() . C = F₄() . C
then not C in X by A6, Th1;
hence F₃() . C = F₄() . C by A3, A8, A12; :: thesis: verum

end;

now :: thesis: for a being object st a in B holds
(F₃() | B) . a = (F₄() | B) . a

let a be object ; :: thesis: ( a in B implies (F₃() | B) . a = (F₄() | B) . a )
assume A13: a in B ; :: thesis: (F₃() | B) . a = (F₄() | B) . a
then reconsider a9 = a as Ordinal by Th9;
( F₃() . a9 = F₄() . a9 & (F₃() | B) . a = F₃() . a ) by A11, A9, A13, FUNCT_1:47;
hence (F₃() | B) . a = (F₄() | B) . a by A10, A13, FUNCT_1:47; :: thesis: verum

end;

then A14: F₃() | B = F₄() | B by A9, A10;
( F₃() . B = F₂((F₃() | B)) & F₄() . B = F₂((F₄() | B)) ) by A1, A2, A7;
hence contradiction by A3, A5, A14; :: thesis: verum