let n be Nat; :: thesis: for D being non empty set
for B being BinOp of D st B is commutative holds
product B,n is commutative
let D be non empty set ; :: thesis: for B being BinOp of D st B is commutative holds
product B,n is commutative
let B be BinOp of D; :: thesis: ( B is commutative implies product B,n is commutative )
assume A1: B is commutative ; :: thesis: product B,n is commutative

now

let x, y be Element of n -tuples_on D; :: thesis: (product B,n) . x,y = (product B,n) . y,x
thus (product B,n) . x,y = B .: x,y by Def1
.= B .: y,x by A1, FINSEQOP:34
.= (product B,n) . y,x by Def1 ; :: thesis: verum

end;

hence product B,n is commutative by BINOP_1:def 2; :: thesis: verum