for n being Nat
for D being non empty set
for B being BinOp of D st B is commutative holds
product (B,n) is commutative