defpred S₁[ object ] means F₅() . $1 <> F₆() . $1;
consider X being set such that
A9: for Y being object holds
( Y in X iff ( Y in F₁() & S₁[Y] ) ) from XBOOLE_0:sch 1();
for b being object st b in X holds
b in F₁() by A9;
then A10: X c= F₁() ;
assume F₅() <> F₆() ; :: thesis: contradiction
then ex a being object st
( a in F₁() & F₅() . a <> F₆() . 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 F₁() by A9, A11;
then A14: B c= F₁() by ORDINAL1:def 2;
then A15: ( dom (F₅() | B) = B & dom (F₆() | B) = B ) by A1, A5, RELAT_1:62;

A16: 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 A17: C in B ; :: thesis: F₅() . C = F₆() . C
then not C in X by A12, ORDINAL1:5;
hence F₅() . C = F₆() . C by A9, A14, A17; :: thesis: verum

end;

A18: 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 A19: a in B ; :: thesis: (F₅() | B) . a = (F₆() | B) . a
( (F₅() | B) . a = F₅() . a & (F₆() | B) . a = F₆() . a ) by A15, A19, FUNCT_1:47;
hence (F₅() | B) . a = (F₆() | B) . a by A16, A19; :: thesis: verum

end;

A20: now :: thesis: ( ex C being Ordinal st B = succ C implies F₅() . B = F₆() . B )

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

end;

now :: thesis: ( B <> 0 & ( for C being Ordinal holds B <> succ C ) implies F₅() . B = F₆() . B )

assume that
A23: B <> 0 and
A24: for C being Ordinal holds B <> succ C ; :: thesis: F₅() . B = F₆() . B
B is limit_ordinal by A24, ORDINAL1:29;
then ( F₅() . B = F₄(B,(F₅() | B)) & F₆() . B = F₄(B,(F₆() | B)) ) by A4, A8, A13, A23;
hence F₅() . B = F₆() . B by A15, A18, FUNCT_1:2; :: thesis: verum

end;

hence contradiction by A2, A6, A9, A11, A20; :: thesis: verum