let D be non empty set ; :: thesis: for o being BinOp of D st o is commutative holds

o .:^2 is commutative

let o be BinOp of D; :: thesis: ( o is commutative implies o .:^2 is commutative )

assume A1: o is commutative ; :: thesis: o .:^2 is commutative

let x, y be Subset of D; :: according to BINOP_1:def 2 :: thesis: (o .:^2) . (x,y) = (o .:^2) . (y,x)

thus (o .:^2) . (x,y) = o .: [:x,y:] by Th44

.= o .: [:y,x:] by A1, Th47

.= (o .:^2) . (y,x) by Th44 ; :: thesis: verum

o .:^2 is commutative

let o be BinOp of D; :: thesis: ( o is commutative implies o .:^2 is commutative )

assume A1: o is commutative ; :: thesis: o .:^2 is commutative

let x, y be Subset of D; :: according to BINOP_1:def 2 :: thesis: (o .:^2) . (x,y) = (o .:^2) . (y,x)

thus (o .:^2) . (x,y) = o .: [:x,y:] by Th44

.= o .: [:y,x:] by A1, Th47

.= (o .:^2) . (y,x) by Th44 ; :: thesis: verum