let G be addGroup; :: thesis: add_inverse G is_an_inverseOp_wrt the addF of G
let h be Element of G; :: according to FINSEQOP:def 1 :: thesis: ( the addF of G . (h,((add_inverse G) . h)) = the_unity_wrt the addF of G & the addF of G . (((add_inverse G) . h),h) = the_unity_wrt the addF of G )
thus the addF of G . (h,((add_inverse G) . h)) = h + (- h) by Def6
.= 0_ G by Def5
.= the_unity_wrt the addF of G by Th21 ; :: thesis: the addF of G . (((add_inverse G) . h),h) = the_unity_wrt the addF of G
thus the addF of G . (((add_inverse G) . h),h) = (- h) + h by Def6
.= 0_ G by Def5
.= the_unity_wrt the addF of G by Th21 ; :: thesis: verum