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),(the_inverseOp_wrt F)) 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),(the_inverseOp_wrt F)) 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),(the_inverseOp_wrt F)) ; :: 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,((the_inverseOp_wrt F) . d2))),(G . (d3,d4))) by A4, Th81
.= F . ((F . (d1,((the_inverseOp_wrt F) . d2))),(F . (d3,((the_inverseOp_wrt F) . d4)))) by A4, Th81
.= F . (d1,(F . (((the_inverseOp_wrt F) . d2),(F . (d3,((the_inverseOp_wrt F) . d4)))))) by A2
.= F . (d1,(F . ((F . (((the_inverseOp_wrt F) . d2),d3)),((the_inverseOp_wrt F) . d4)))) by A2
.= F . (d1,(F . ((F . (d3,((the_inverseOp_wrt F) . d2))),((the_inverseOp_wrt F) . d4)))) by A1
.= F . (d1,(F . (d3,(F . (((the_inverseOp_wrt F) . d2),((the_inverseOp_wrt F) . d4)))))) by A2
.= F . ((F . (d1,d3)),(F . (((the_inverseOp_wrt F) . d2),((the_inverseOp_wrt F) . d4)))) by A2
.= F . ((F . (d1,d3)),((the_inverseOp_wrt F) . (F . (d2,d4)))) by A5
.= G . ((F . (d1,d3)),(F . (d2,d4))) by A4, Th81 ; :: thesis: verum