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

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