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

.= F . (d1,(F . ((F . (d2,d3)),d4))) by A2

.= F . (d1,(F . ((F . (d3,d2)),d4))) by A1

.= F . (d1,(F . (d3,(F . (d2,d4))))) by A2

.= F . ((F . (d1,d3)),(F . (d2,d4))) by A2 ; :: thesis: verum

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

.= F . (d1,(F . ((F . (d2,d3)),d4))) by A2

.= F . (d1,(F . ((F . (d3,d2)),d4))) by A1

.= F . (d1,(F . (d3,(F . (d2,d4))))) by A2

.= F . ((F . (d1,d3)),(F . (d2,d4))) by A2 ; :: thesis: verum