let o1, o2 be BinOp of {0,1,2}; ( ( for a, b being Element of {0,1,2} holds o1 . (a,b) = a * b ) & ( for a, b being Element of {0,1,2} holds o2 . (a,b) = a * b ) implies o1 = o2 )
assume that
A3:
for a, b being Element of {0,1,2} holds o1 . (a,b) = a * b
and
A4:
for a, b being Element of {0,1,2} holds o2 . (a,b) = a * b
; o1 = o2
now for a, b being Element of {0,1,2} holds o1 . (a,b) = o2 . (a,b)let a,
b be
Element of
{0,1,2};
o1 . (a,b) = o2 . (a,b)thus o1 . (
a,
b) =
a * b
by A3
.=
o2 . (
a,
b)
by A4
;
verum end;
hence
o1 = o2
by BINOP_1:2; verum