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