for D being non empty set
for F being BinOp of D
for i being Nat st F is having_a_unity holds
F "**" (i |-> (the_unity_wrt F)) = the_unity_wrt F