theorem Th71: :: AFINSQ_2:72

for D being non empty set
for b being BinOp of D st b is having_a_unity holds
b "**" (<%> D) = the_unity_wrt b