let D be non empty set ; :: thesis: for B being BinOp of D
for d1, d2 being Element of D st B is having_a_unity & B is associative & B is commutative & B is having_an_inverseOp holds
(the_inverseOp_wrt B) . (B . (d1,d2)) = B . (((the_inverseOp_wrt B) . d1),((the_inverseOp_wrt B) . d2))
let B be BinOp of D; :: thesis: for d1, d2 being Element of D st B is having_a_unity & B is associative & B is commutative & B is having_an_inverseOp holds
(the_inverseOp_wrt B) . (B . (d1,d2)) = B . (((the_inverseOp_wrt B) . d1),((the_inverseOp_wrt B) . d2))
let d1, d2 be Element of D; :: thesis: ( B is having_a_unity & B is associative & B is commutative & B is having_an_inverseOp implies (the_inverseOp_wrt B) . (B . (d1,d2)) = B . (((the_inverseOp_wrt B) . d1),((the_inverseOp_wrt B) . d2)) )
set I = the_inverseOp_wrt B;
assume A1: ( B is having_a_unity & B is associative & B is commutative & B is having_an_inverseOp ) ; :: thesis: (the_inverseOp_wrt B) . (B . (d1,d2)) = B . (((the_inverseOp_wrt B) . d1),((the_inverseOp_wrt B) . d2))
B . ((B . (d1,d2)),(B . (((the_inverseOp_wrt B) . d1),((the_inverseOp_wrt B) . d2)))) = B . ((B . (d2,d1)),(B . (((the_inverseOp_wrt B) . d1),((the_inverseOp_wrt B) . d2)))) by A1, BINOP_1:def 2
.= B . ((B . ((B . (d2,d1)),((the_inverseOp_wrt B) . d1))),((the_inverseOp_wrt B) . d2)) by A1, BINOP_1:def 3
.= B . ((B . (d2,(B . (d1,((the_inverseOp_wrt B) . d1))))),((the_inverseOp_wrt B) . d2)) by A1, BINOP_1:def 3
.= B . ((B . (d2,(the_unity_wrt B))),((the_inverseOp_wrt B) . d2)) by A1, FINSEQOP:59
.= B . (d2,((the_inverseOp_wrt B) . d2)) by A1, SETWISEO:15
.= the_unity_wrt B by A1, FINSEQOP:59 ;
hence (the_inverseOp_wrt B) . (B . (d1,d2)) = B . (((the_inverseOp_wrt B) . d1),((the_inverseOp_wrt B) . d2)) by A1, FINSEQOP:60; :: thesis: verum