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 13 :: 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, Th4
.= (o,D .: A) . g,f by Def2 ; :: thesis: verum