let A be set ; :: thesis: 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 ; :: thesis: for o being BinOp of D st o is commutative holds
(o,D) .: A is commutative
let o be BinOp of D; :: thesis: ( o is commutative implies (o,D) .: A is commutative )
assume A1: o is commutative ; :: thesis: (o,D) .: A is commutative
set h = (o,D) .: A;
let f, g be Element of Funcs (A,D); :: according to BINOP_1:def 2 :: thesis: ((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 ; :: thesis: verum