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 that
A9: for c, d being Subset of X holds f . c,d = c \+\ d and
A10: for c, d being Subset of X holds g . c,d = c \+\ d ; :: thesis: f = g
dom f = [:(bool X),(bool X):] by FUNCT_2:def 1;
then A11: dom f = dom g by FUNCT_2:def 1;
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 A12: x in dom f ; :: thesis: f . x = g . x
consider y, z being set such that
A13: y in bool X and
A14: z in bool X and
A15: x = [y,z] by A12, ZFMISC_1:def 2;
reconsider y = y as Subset of X by A13;
reconsider z = z as Subset of X by A14;
( f . y,z = y \+\ z & g . y,z = y \+\ z ) by A9, A10;
hence f . x = g . x by A15; :: thesis: verum

end;

hence f = g by A11, FUNCT_1:9; :: thesis: verum