theorem Th10: :: MONOID_1:10

for A being set
for D being non empty set
for o being BinOp of D st o is having_a_unity holds
( the_unity_wrt ((o,D) .: A) = A --> (the_unity_wrt o) & (o,D) .: A is having_a_unity )