let D be non empty set ; :: 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_unity_wrt F) = the_unity_wrt F
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_unity_wrt F) = the_unity_wrt F )
assume that
A1: F is having_a_unity and
A2: ( F is associative & F is having_an_inverseOp ) ; :: thesis: (the_inverseOp_wrt F) . (the_unity_wrt F) = the_unity_wrt F
set e = the_unity_wrt F;
F . ((the_unity_wrt F),(the_unity_wrt F)) = the_unity_wrt F by A1, SETWISEO:15;
hence (the_inverseOp_wrt F) . (the_unity_wrt F) = the_unity_wrt F by A1, A2, Th60; :: thesis: verum