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

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 :: thesis: for a, b being Element of {0,1,2} holds o1 . (a,b) = o2 . (a,b)

hence
o1 = o2
by BINOP_1:2; :: thesis: verumlet 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;thus o1 . (a,b) = a + b by A1

.= o2 . (a,b) by A2 ; :: thesis: verum