for X, Y being set
for D being non empty set
for o being BinOp of D st o is commutative holds
o .: [:X,Y:] = o .: [:Y,X:]