assume F₅() <> F₆() ; :: thesis: contradiction
then consider a being set such that
A9: ( a in F₁() & F₅() . a <> F₆() . a ) by A1, A5, FUNCT_1:9;
defpred S₁[ set ] means F₅() . $1 <> F₆() . $1;
consider X being set such that
A10: for Y being set holds
( Y in X iff ( Y in F₁() & S₁[Y] ) ) from XBOOLE_0:sch 1();
A11: X <> {} by A9, A10;
for b being set st b in X holds
b in F₁() by A10;
then X c= F₁() by TARSKI:def 3;
then consider B being Ordinal such that
A12: ( B in X & ( for C being Ordinal st C in X holds
B c= C ) ) by A11, ORDINAL1:32;
A13: ( B in F₁() & F₅() . B <> F₆() . B ) by A10, A12;
then A14: B c= F₁() by ORDINAL1:def 2;

A15: now

let C be Ordinal; :: thesis: ( C in B implies F₅() . C = F₆() . C )
assume A16: C in B ; :: thesis: F₅() . C = F₆() . C
then not C in X by A12, ORDINAL1:7;
hence F₅() . C = F₆() . C by A10, A14, A16; :: thesis: verum

end;

A17: ( dom (F₅() | B) = B & dom (F₆() | B) = B ) by A1, A5, A14, RELAT_1:91;

A18: now

let a be set ; :: thesis: ( a in B implies (F₅() | B) . a = (F₆() | B) . a )
assume A19: a in B ; :: thesis: (F₅() | B) . a = (F₆() | B) . a
then reconsider a' = a as Ordinal ;
( (F₅() | B) . a = F₅() . a & (F₆() | B) . a = F₆() . a ) by A17, A19, FUNCT_1:70;
hence (F₅() | B) . a = (F₆() | B) . a by A15, A19; :: thesis: verum

end;

A21: now

given C being Ordinal such that A22: B = succ C ; :: thesis: F₅() . B = F₆() . B
A23: ( F₅() . B = F₃(C,(F₅() . C)) & F₆() . B = F₃(C,(F₆() . C)) & C in B ) by A3, A7, A13, A22, ORDINAL1:10;
( F₅() . C = (F₅() | B) . C & F₆() . C = (F₆() | B) . C ) by FUNCT_1:72, A22, ORDINAL1:10;
hence F₅() . B = F₆() . B by A18, A23; :: thesis: verum

end;

now

assume A24: ( B <> {} & ( for C being Ordinal holds B <> succ C ) ) ; :: thesis: F₅() . B = F₆() . B
then B is limit_ordinal by ORDINAL1:42;
then ( F₅() . B = F₄(B,(F₅() | B)) & F₆() . B = F₄(B,(F₆() | B)) ) by A4, A8, A13, A24;
hence F₅() . B = F₆() . B by A17, A18, FUNCT_1:9; :: thesis: verum

end;

hence contradiction by A2, A6, A10, A12, A21; :: thesis: verum