let G be Group; :: thesis: inverse_op G is_an_inverseOp_wrt the multF of G
let h be Element of G; :: according to FINSEQOP:def 1 :: thesis: ( the multF of G . h,((inverse_op G) . h) = the_unity_wrt the multF of G & the multF of G . ((inverse_op G) . h),h = the_unity_wrt the multF of G )
thus the multF of G . h,((inverse_op G) . h) = h * (h " ) by Def7
.= 1_ G by Def6
.= the_unity_wrt the multF of G by Th33 ; :: thesis: the multF of G . ((inverse_op G) . h),h = the_unity_wrt the multF of G
thus the multF of G . ((inverse_op G) . h),h = (h " ) * h by Def7
.= 1_ G by Def6
.= the_unity_wrt the multF of G by Th33 ; :: thesis: verum