let D be non empty set ; :: thesis: for F, G being BinOp of D st F is commutative & F is associative & F is having_a_unity & F is having_an_inverseOp & G = F * ((id D),) holds
for d1, d2, d3, d4 being Element of D holds F . ((G . (d1,d2)),(G . (d3,d4))) = G . ((F . (d1,d3)),(F . (d2,d4)))

let F, G be BinOp of D; :: thesis: ( F is commutative & F is associative & F is having_a_unity & F is having_an_inverseOp & G = F * ((id D),) implies for d1, d2, d3, d4 being Element of D holds F . ((G . (d1,d2)),(G . (d3,d4))) = G . ((F . (d1,d3)),(F . (d2,d4))) )
assume that
A1: F is commutative and
A2: F is associative and
A3: ( F is having_a_unity & F is having_an_inverseOp ) and
A4: G = F * ((id D),) ; :: thesis: for d1, d2, d3, d4 being Element of D holds F . ((G . (d1,d2)),(G . (d3,d4))) = G . ((F . (d1,d3)),(F . (d2,d4)))
set u = the_inverseOp_wrt F;
A5: the_inverseOp_wrt F is_distributive_wrt F by A1, A2, A3, Th63;
let d1, d2, d3, d4 be Element of D; :: thesis: F . ((G . (d1,d2)),(G . (d3,d4))) = G . ((F . (d1,d3)),(F . (d2,d4)))
thus F . ((G . (d1,d2)),(G . (d3,d4))) = F . ((F . (d1,( . d2))),(G . (d3,d4))) by
.= F . ((F . (d1,( . d2))),(F . (d3,( . d4)))) by
.= 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
.= F . ((F . (d1,d3)),( . (F . (d2,d4)))) by A5
.= G . ((F . (d1,d3)),(F . (d2,d4))) by ; :: thesis: verum