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
A1:
for a, b being Element of {0,1,2} holds o1 . (a,b) = a + b
and
A2:
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 A1
.=
o2 . (
a,
b)
by A2
;
verum end;
hence
o1 = o2
by BINOP_1:2; verum