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

(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