theorem Th52: :: MONOID_1:52

for D being non empty set

for o being BinOp of D

for a being Element of D st a is_a_unity_wrt o holds

( {a} is_a_unity_wrt o .:^2 & o .:^2 is having_a_unity & the_unity_wrt (o .:^2) = {a} )

for o being BinOp of D

for a being Element of D st a is_a_unity_wrt o holds

( {a} is_a_unity_wrt o .:^2 & o .:^2 is having_a_unity & the_unity_wrt (o .:^2) = {a} )