defpred S₁[ set ] means F₃() . $1 <> F₄() . $1;
consider X being set such that
A3: for x being set holds
( x in X iff ( x in F₁() & S₁[x] ) ) from XBOOLE_0:sch 1();
for b being set st b in X holds
b in F₁() by A3;
then A4: X c= F₁() by TARSKI:def 3;
assume F₃() <> F₄() ; :: thesis: contradiction
then ex a being set st
( a in F₁() & F₃() . a <> F₄() . a ) by A1, A2, FUNCT_1:2;
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, Th32;
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

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, Th7;
hence F₃() . C = F₄() . C by A3, A8, A12; :: thesis: verum

end;

now

let a be set ; :: 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 Th23;
( 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, FUNCT_1:2;
( F₃() . B = F₂((F₃() | B)) & F₄() . B = F₂((F₄() | B)) ) by A1, A2, A7;
hence contradiction by A3, A5, A14; :: thesis: verum