let D be non empty set ; :: thesis: for F being BinOp of D st F is commutative & F is associative holds
for d1, d2, d3, d4 being Element of D holds F . (F . d1,d2),(F . d3,d4) = F . (F . d1,d3),(F . d2,d4)
let F be BinOp of D; :: thesis: ( F is commutative & F is associative implies for d1, d2, d3, d4 being Element of D holds F . (F . d1,d2),(F . d3,d4) = F . (F . d1,d3),(F . d2,d4) )
assume that
A1: F is commutative and
A2: F is associative ; :: thesis: for d1, d2, d3, d4 being Element of D holds F . (F . d1,d2),(F . d3,d4) = F . (F . d1,d3),(F . d2,d4)
let d1, d2, d3, d4 be Element of D; :: thesis: F . (F . d1,d2),(F . d3,d4) = F . (F . d1,d3),(F . d2,d4)
thus F . (F . d1,d2),(F . d3,d4) = F . d1,(F . d2,(F . d3,d4)) by A2, BINOP_1:def 3
.= F . d1,(F . (F . d2,d3),d4) by A2, BINOP_1:def 3
.= F . d1,(F . (F . d3,d2),d4) by A1, BINOP_1:def 2
.= F . d1,(F . d3,(F . d2,d4)) by A2, BINOP_1:def 3
.= F . (F . d1,d3),(F . d2,d4) by A2, BINOP_1:def 3 ; :: thesis: verum