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 Def6
.= 1_ G by Def5
.= the_unity_wrt the multF of G by Th21 ; :: 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 Def6
.= 1_ G by Def5
.= the_unity_wrt the multF of G by Th21 ; :: thesis: verum