theorem Th103: :: HILB10_7:103

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