let D be non empty set ; :: thesis: for F being BinOp of D st F is having_a_unity & F is associative & F is commutative & F is having_an_inverseOp holds
the_inverseOp_wrt F is_distributive_wrt F

let F be BinOp of D; :: thesis: ( F is having_a_unity & F is associative & F is commutative & F is having_an_inverseOp implies the_inverseOp_wrt F is_distributive_wrt F )
assume that
A1: F is having_a_unity and
A2: F is associative and
A3: F is commutative and
A4: F is having_an_inverseOp ; :: thesis:
let d1 be Element of D; :: according to BINOP_1:def 20 :: thesis: for b1 being Element of D holds . (F . (d1,b1)) = F . (( . d1),( . b1))
let d2 be Element of D; :: thesis: . (F . (d1,d2)) = F . (( . d1),( . d2))
set e = the_unity_wrt F;
set u = the_inverseOp_wrt F;
F . ((F . (( . d1),( . d2))),(F . (d1,d2))) = F . (( . d1),(F . (( . d2),(F . (d1,d2))))) by A2
.= F . (( . d1),(F . ((F . (( . d2),d1)),d2))) by A2
.= F . (( . d1),(F . ((F . (d1,( . d2))),d2))) by A3
.= F . (( . d1),(F . (d1,(F . (( . d2),d2))))) by A2
.= F . (( . d1),(F . (d1,()))) by A1, A2, A4, Th59
.= F . ((F . (( . d1),d1)),()) by A2
.= F . ((),()) by A1, A2, A4, Th59
.= the_unity_wrt F by ;
hence (the_inverseOp_wrt F) . (F . (d1,d2)) = F . (( . d1),( . d2)) by A1, A2, A4, Th60; :: thesis: verum