let H1, H2 be BinOp of (n -tuples_on BOOLEAN); :: thesis: ( ( for x, y being Element of n -tuples_on BOOLEAN holds H1 . (x,y) = Op-XOR (x,y) ) & ( for x, y being Element of n -tuples_on BOOLEAN holds H2 . (x,y) = Op-XOR (x,y) ) implies H1 = H2 )
assume A2: for x, y being Element of n -tuples_on BOOLEAN holds H1 . (x,y) = Op-XOR (x,y) ; :: thesis: ( ex x, y being Element of n -tuples_on BOOLEAN st not H2 . (x,y) = Op-XOR (x,y) or H1 = H2 )
assume A3: for x, y being Element of n -tuples_on BOOLEAN holds H2 . (x,y) = Op-XOR (x,y) ; :: thesis: H1 = H2
for x, y being Element of n -tuples_on BOOLEAN holds H1 . (x,y) = H2 . (x,y)

proof

let x, y be Element of n -tuples_on BOOLEAN; :: thesis: H1 . (x,y) = H2 . (x,y)
thus H1 . (x,y) = Op-XOR (x,y) by A2
.= H2 . (x,y) by A3 ; :: thesis: verum

end;

hence H1 = H2 by BINOP_1:2; :: thesis: verum