let n be Nat; 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 ; for B being BinOp of D st B is commutative holds
product (B,n) is commutative
let B be BinOp of D; ( B is commutative implies product (B,n) is commutative )
assume A1:
B is commutative
; product (B,n) is commutative
now 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;
(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
;
verum end;
hence
product (B,n) is commutative
; verum