theorem :: FINSOP_1:15

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