let G be non empty multMagma ; :: thesis: ( G is associative & G is Group-like implies G is invertible )
assume ( G is associative & G is Group-like ) ; :: thesis: G is invertible
then reconsider G = G as non empty Group-like associative multMagma ;
( G is unital & G is associative & H₂(G) is having_an_inverseOp ) by GROUP_1:36;
hence G is invertible by Th17; :: thesis: verum