let H1, H2 be BinOp of (n -tuples_on BOOLEAN); ( ( 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)
; ( 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)
; H1 = H2
for x, y being Element of n -tuples_on BOOLEAN holds H1 . (x,y) = H2 . (x,y)
hence
H1 = H2
by BINOP_1:2; verum