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

( F . (((the_inverseOp_wrt F) . d),d) = the_unity_wrt F & F . (d,((the_inverseOp_wrt F) . d)) = the_unity_wrt F )

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

( F . (((the_inverseOp_wrt F) . d),d) = the_unity_wrt F & F . (d,((the_inverseOp_wrt F) . d)) = 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 ( F . (((the_inverseOp_wrt F) . d),d) = the_unity_wrt F & F . (d,((the_inverseOp_wrt F) . d)) = the_unity_wrt F ) )

assume ( F is having_a_unity & F is associative & F is having_an_inverseOp ) ; :: thesis: ( F . (((the_inverseOp_wrt F) . d),d) = the_unity_wrt F & F . (d,((the_inverseOp_wrt F) . d)) = the_unity_wrt F )

then the_inverseOp_wrt F is_an_inverseOp_wrt F by Def3;

hence ( F . (((the_inverseOp_wrt F) . d),d) = the_unity_wrt F & F . (d,((the_inverseOp_wrt F) . d)) = the_unity_wrt F ) ; :: thesis: verum

for F being BinOp of D st F is having_a_unity & F is associative & F is having_an_inverseOp holds

( F . (((the_inverseOp_wrt F) . d),d) = the_unity_wrt F & F . (d,((the_inverseOp_wrt F) . d)) = the_unity_wrt F )

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

( F . (((the_inverseOp_wrt F) . d),d) = the_unity_wrt F & F . (d,((the_inverseOp_wrt F) . d)) = 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 ( F . (((the_inverseOp_wrt F) . d),d) = the_unity_wrt F & F . (d,((the_inverseOp_wrt F) . d)) = the_unity_wrt F ) )

assume ( F is having_a_unity & F is associative & F is having_an_inverseOp ) ; :: thesis: ( F . (((the_inverseOp_wrt F) . d),d) = the_unity_wrt F & F . (d,((the_inverseOp_wrt F) . d)) = the_unity_wrt F )

then the_inverseOp_wrt F is_an_inverseOp_wrt F by Def3;

hence ( F . (((the_inverseOp_wrt F) . d),d) = the_unity_wrt F & F . (d,((the_inverseOp_wrt F) . d)) = the_unity_wrt F ) ; :: thesis: verum