let A be set ; for D being non empty set
for o being BinOp of D st o is commutative holds
(o,D) .: A is commutative
let D be non empty set ; for o being BinOp of D st o is commutative holds
(o,D) .: A is commutative
let o be BinOp of D; ( o is commutative implies (o,D) .: A is commutative )
assume A1:
o is commutative
; (o,D) .: A is commutative
set h = (o,D) .: A;
let f, g be Element of Funcs (A,D); BINOP_1:def 2 ((o,D) .: A) . (f,g) = ((o,D) .: A) . (g,f)
thus ((o,D) .: A) . (f,g) =
o .: (f,g)
by Def2
.=
o .: (g,f)
by A1, Th3
.=
((o,D) .: A) . (g,f)
by Def2
; verum