defpred S1[ object ] means F3() . $1 <> F4() . $1;
consider X being set such that
A3: for x being object holds
( x in X iff ( x in F1() & S1[x] ) ) from XBOOLE_0:sch 1();
 for b being object st b in X holds
b in F1() by A3;
then A4: X c= F1() ;
assume F3() <> F4() ; :: thesis: contradiction
then ex a being object st
( a in F1() & F3() . a <> F4() . a ) by A1, A2;
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, Th16;
A7: B in F1() by A3, A5;
then A8: B c= F1() by Def2;
then A9: dom (F3() | B) = B by A1, RELAT_1:62;
A10: dom (F4() | B) = B by A2, A8, RELAT_1:62;
A11: now :: thesis: for C being Ordinal st C in B holds
F3() . C = F4() . C
let C be Ordinal; :: thesis: ( C in B implies F3() . C = F4() . C )
assume A12: C in B ; :: thesis: F3() . C = F4() . C
then not C in X by A6, Th1;
hence F3() . C = F4() . C by A3, A8, A12; :: thesis: verum
end;
now :: thesis: for a being object st a in B holds
(F3() | B) . a = (F4() | B) . a
let a be object ; :: thesis: ( a in B implies (F3() | B) . a = (F4() | B) . a )
assume A13: a in B ; :: thesis: (F3() | B) . a = (F4() | B) . a
then reconsider a9 = a as Ordinal by Th9;
( F3() . a9 = F4() . a9 & (F3() | B) . a = F3() . a ) by A11, A9, A13, FUNCT_1:47;
hence (F3() | B) . a = (F4() | B) . a by A10, A13, FUNCT_1:47; :: thesis: verum
end;
then A14: F3() | B = F4() | B by A9, A10;
( F3() . B = F2((F3() | B)) & F4() . B = F2((F4() | B)) ) by A1, A2, A7;
hence contradiction by A3, A5, A14; :: thesis: verum