let D be non empty set ; :: thesis: for d1, d2, d3 being Element of D
for g being BinOp of D st g is commutative holds
g "**" <*d1,d2,d3*> = g "**" <*d2,d1,d3*>
let d1, d2, d3 be Element of D; :: thesis: for g being BinOp of D st g is commutative holds
g "**" <*d1,d2,d3*> = g "**" <*d2,d1,d3*>
let g be BinOp of D; :: thesis: ( g is commutative implies g "**" <*d1,d2,d3*> = g "**" <*d2,d1,d3*> )
assume A1: g is commutative ; :: thesis: g "**" <*d1,d2,d3*> = g "**" <*d2,d1,d3*>
thus g "**" <*d1,d2,d3*> = g . ((g . (d1,d2)),d3) by Th14
.= g . ((g . (d2,d1)),d3) by A1, BINOP_1:def 2
.= g "**" <*d2,d1,d3*> by Th14 ; :: thesis: verum