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