theorem :: FINSOP_1:13

for D being non empty set
for d1, d2 being Element of D
for g being BinOp of D st g is commutative holds
g "**" <*d1,d2*> = g "**" <*d2,d1*>