for X being non empty set
for F being BinOp of X st F is having_a_unity holds
for x being Element of X holds
( F . ((the_unity_wrt F),x) = x & F . (x,(the_unity_wrt F)) = x )