assume F₃() <> F₄() ; :: thesis: contradiction
then consider a being set such that
A3: ( a in F₁() & F₃() . a <> F₄() . a ) by A1, A2, FUNCT_1:9;
defpred S₁[ set ] means F₃() . $1 <> F₄() . $1;
consider X being set such that
A4: for x being set holds
( x in X iff ( x in F₁() & S₁[x] ) ) from XBOOLE_0:sch 1();
A5: X <> {} by A3, A4;
for b being set st b in X holds
b in F₁() by A4;
then X c= F₁() by TARSKI:def 3;
then consider B being Ordinal such that
A6: ( B in X & ( for C being Ordinal st C in X holds
B c= C ) ) by A5, Th32;
A7: ( B in F₁() & F₃() . B <> F₄() . B ) by A4, A6;
then A8: B c= F₁() by Def2;

A9: now

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

end;

A11: ( dom (F₃() | B) = B & dom (F₄() | B) = B ) by A1, A2, A8, RELAT_1:91;

now

let a be set ; :: thesis: ( a in B implies (F₃() | B) . a = (F₄() | B) . a )
assume A12: a in B ; :: thesis: (F₃() | B) . a = (F₄() | B) . a
then reconsider a' = a as Ordinal by Th23;
A13: F₃() . a' = F₄() . a' by A9, A12;
( (F₃() | B) . a = F₃() . a & (F₄() | B) . a = F₄() . a ) by A11, A12, FUNCT_1:70;
hence (F₃() | B) . a = (F₄() | B) . a by A13; :: thesis: verum

end;

then A14: F₃() | B = F₄() | B by A11, FUNCT_1:9;
( F₃() . B = F₂((F₃() | B)) & F₄() . B = F₂((F₄() | B)) ) by A1, A2, A7;
hence contradiction by A4, A6, A14; :: thesis: verum