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 :: thesis: for x, y being Element of n -tuples_on D holds (product (B,n)) . (x,y) = (product (B,n)) . (y,x)

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:33
.= (product (B,n)) . (y,x) by Def1 ; :: thesis: verum

end;

hence product (B,n) is commutative ; :: thesis: verum