let o1, o2 be BinOp of {1,2,3}; ( ( for x, y being Element of {1,2,3} holds o1 . (x,y) = x example32"/\" y ) & ( for x, y being Element of {1,2,3} holds o2 . (x,y) = x example32"/\" y ) implies o1 = o2 )
assume that
A1:
for x, y being Element of {1,2,3} holds o1 . (x,y) = x example32"/\" y
and
A2:
for x, y being Element of {1,2,3} holds o2 . (x,y) = x example32"/\" y
; o1 = o2
hence
o1 = o2
by BINOP_1:2; verum