let f, g be BinOp of (bool X); :: thesis: ( ( for c, d being Subset of X holds f . c,d = c \+\ d ) & ( for c, d being Subset of X holds g . c,d = c \+\ d ) implies f = g )
assume A3: ( ( for c, d being Subset of X holds f . c,d = c \+\ d ) & ( for c, d being Subset of X holds g . c,d = c \+\ d ) ) ; :: thesis: f = g
A4: for x being set st x in dom f holds
f . x = g . x

proof

let x be set ; :: thesis: ( x in dom f implies f . x = g . x )
assume x in dom f ; :: thesis: f . x = g . x
then consider y, z being set such that
A5: y in bool X and
A6: z in bool X and
A7: x = [y,z] by ZFMISC_1:def 2;
reconsider z = z as Subset of X by A6;
reconsider y = y as Subset of X by A5;
( f . y,z = y \+\ z & g . y,z = y \+\ z ) by A3;
hence f . x = g . x by A7; :: thesis: verum

end;

dom f = [:(bool X),(bool X):] by FUNCT_2:def 1;
then dom f = dom g by FUNCT_2:def 1;
hence f = g by A4, FUNCT_1:9; :: thesis: verum