let D be non empty set ; :: thesis: for d being Element of D
for F being BinOp of D st F is associative & F is having_a_unity & F is having_an_inverseOp holds
(F * ((id D),(the_inverseOp_wrt F))) . (d,d) = the_unity_wrt F
let d be Element of D; :: thesis: for F being BinOp of D st F is associative & F is having_a_unity & F is having_an_inverseOp holds
(F * ((id D),(the_inverseOp_wrt F))) . (d,d) = the_unity_wrt F
let F be BinOp of D; :: thesis: ( F is associative & F is having_a_unity & F is having_an_inverseOp implies (F * ((id D),(the_inverseOp_wrt F))) . (d,d) = the_unity_wrt F )
assume A1: ( F is associative & F is having_a_unity & F is having_an_inverseOp ) ; :: thesis: (F * ((id D),(the_inverseOp_wrt F))) . (d,d) = the_unity_wrt F
set u = the_inverseOp_wrt F;
thus (F * ((id D),(the_inverseOp_wrt F))) . (d,d) = F . (d,((the_inverseOp_wrt F) . d)) by Th81
.= the_unity_wrt F by A1, Th59 ; :: thesis: verum