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

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)

hence
product (B,n) is commutative
; :: thesis: verumlet 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;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