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 object st x in dom f holds

f . x = g . x

then dom f = dom g by FUNCT_2:def 1;

hence f = g by A4; :: thesis: verum

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 object st x in dom f holds

f . x = g . x

proof

dom f = [:(bool X),(bool X):]
by FUNCT_2:def 1;
let x be object ; :: 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 object 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;assume x in dom f ; :: thesis: f . x = g . x

then consider y, z being object 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

then dom f = dom g by FUNCT_2:def 1;

hence f = g by A4; :: thesis: verum