let o1, o2 be BinOp of {0,1,2,3,4}; :: thesis: ( ( for x, y being Element of {0,1,2,3,4} holds o1 . (x,y) = x ex1234"\/" y ) & ( for x, y being Element of {0,1,2,3,4} holds o2 . (x,y) = x ex1234"\/" y ) implies o1 = o2 )
assume that
A1: for x, y being Element of {0,1,2,3,4} holds o1 . (x,y) = x ex1234"\/" y and
A2: for x, y being Element of {0,1,2,3,4} holds o2 . (x,y) = x ex1234"\/" y ; :: thesis: o1 = o2

now :: thesis: for x, y being Element of {0,1,2,3,4} holds o1 . (x,y) = o2 . (x,y)

let x, y be Element of {0,1,2,3,4}; :: thesis: o1 . (x,y) = o2 . (x,y)
thus o1 . (x,y) = x ex1234"\/" y by A1
.= o2 . (x,y) by A2 ; :: thesis: verum

end;

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