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, Th67;
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, Th87
.= F . (F . d1,((the_inverseOp_wrt F) . d2)),(F . d3,((the_inverseOp_wrt F) . d4)) by A4, Th87
.= F . d1,(F . ((the_inverseOp_wrt F) . d2),(F . d3,((the_inverseOp_wrt F) . d4))) by A2, BINOP_1:def 3
.= F . d1,(F . (F . ((the_inverseOp_wrt F) . d2),d3),((the_inverseOp_wrt F) . d4)) by A2, BINOP_1:def 3
.= F . d1,(F . (F . d3,((the_inverseOp_wrt F) . d2)),((the_inverseOp_wrt F) . d4)) by A1, BINOP_1:def 2
.= F . d1,(F . d3,(F . ((the_inverseOp_wrt F) . d2),((the_inverseOp_wrt F) . d4))) by A2, BINOP_1:def 3
.= F . (F . d1,d3),(F . ((the_inverseOp_wrt F) . d2),((the_inverseOp_wrt F) . d4)) by A2, BINOP_1:def 3
.= F . (F . d1,d3),((the_inverseOp_wrt F) . (F . d2,d4)) by A5, BINOP_1:def 12
.= G . (F . d1,d3),(F . d2,d4) by A4, Th87 ; :: thesis: verum