theorem Th2: :: HILB10_7:2

for D being non empty set
for d1, d2 being Element of D
for B being BinOp of D st B is having_a_unity & B is associative & B is commutative & B is having_an_inverseOp holds
( B . (((the_inverseOp_wrt B) . d1),d2) = (the_inverseOp_wrt B) . (B . (d1,((the_inverseOp_wrt B) . d2))) & B . (d1,((the_inverseOp_wrt B) . d2)) = (the_inverseOp_wrt B) . (B . (((the_inverseOp_wrt B) . d1),d2)) )