theorem :: MONOID_0:62

for D being non empty set
for a, b being Element of (D *+^+<0>) holds a [*] b = a ^ b