let o1, o2 be BinOp of {0 ,1,2}; :: thesis: ( ( 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 ; :: thesis: o1 = o2

now

let a, b be Element of {0 ,1,2}; :: thesis: o1 . a,b = o2 . a,b
thus o1 . a,b = a + b by A1
.= o2 . a,b by A2 ; :: thesis: verum

end;

hence o1 = o2 by BINOP_1:2; :: thesis: verum