defpred S1[ object ] means F5() . $1 <> F6() . $1;
consider X being set such that
A9: for Y being object holds
( Y in X iff ( Y in F1() & S1[Y] ) ) from XBOOLE_0:sch 1();
 for b being object st b in X holds
b in F1() by A9;
then A10: X c= F1() ;
assume F5() <> F6() ; :: thesis: contradiction
then ex a being object st
( a in F1() & F5() . a <> F6() . 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 F1() by A9, A11;
then A14: B c= F1() by ORDINAL1:def 2;
then A15: ( dom (F5() | B) = B & dom (F6() | B) = B ) by A1, A5, RELAT_1:62;
A16: now :: thesis: for C being Ordinal st C in B holds
F5() . C = F6() . C
let C be Ordinal; :: thesis: ( C in B implies F5() . C = F6() . C )
assume A17: C in B ; :: thesis: F5() . C = F6() . C
then not C in X by A12, ORDINAL1:5;
hence F5() . C = F6() . C by A9, A14, A17; :: thesis: verum
end;
A18: now :: thesis: for a being object st a in B holds
(F5() | B) . a = (F6() | B) . a
let a be object ; :: thesis: ( a in B implies (F5() | B) . a = (F6() | B) . a )
assume A19: a in B ; :: thesis: (F5() | B) . a = (F6() | B) . a
( (F5() | B) . a = F5() . a & (F6() | B) . a = F6() . a ) by A15, A19, FUNCT_1:47;
hence (F5() | B) . a = (F6() | B) . a by A16, A19; :: thesis: verum
end;
A20: now :: thesis: ( ex C being Ordinal st B = succ C implies F5() . B = F6() . B )
given C being Ordinal such that A21: B = succ C ; :: thesis: F5() . B = F6() . B
A22: ( F5() . C = (F5() | B) . C & F6() . C = (F6() | B) . C ) by A21, FUNCT_1:49, ORDINAL1:6;
( F5() . B = F3(C,(F5() . C)) & F6() . B = F3(C,(F6() . C)) ) by A3, A7, A13, A21;
hence F5() . B = F6() . B by A18, A21, A22, ORDINAL1:6; :: thesis: verum
end;
now :: thesis: ( B <> 0 & ( for C being Ordinal holds B <> succ C ) implies F5() . B = F6() . B )
assume that
A23: B <> 0 and
A24: for C being Ordinal holds B <> succ C ; :: thesis: F5() . B = F6() . B
B is limit_ordinal by A24, ORDINAL1:29;
then ( F5() . B = F4(B,(F5() | B)) & F6() . B = F4(B,(F6() | B)) ) by A4, A8, A13, A23;
hence F5() . B = F6() . B by A15, A18, FUNCT_1:2; :: thesis: verum
end;
hence contradiction by A2, A6, A9, A11, A20; :: thesis: verum