let G be non empty multMagma ; :: thesis: ( G is invertible iff ( G is left-invertible & G is right-invertible ) )
thus ( G is invertible implies ( G is left-invertible & G is right-invertible ) ) :: thesis: ( G is left-invertible & G is right-invertible implies G is invertible )

proof

assume H₂(G) is invertible ; :: according to MONOID_0:def 16 :: thesis: ( G is left-invertible & G is right-invertible )
hence ( H₂(G) is left-invertible & H₂(G) is right-invertible ) by Th1; :: according to MONOID_0:def 14,MONOID_0:def 15 :: thesis: verum

end;

assume ( H₂(G) is left-invertible & H₂(G) is right-invertible ) ; :: according to MONOID_0:def 14,MONOID_0:def 15 :: thesis: G is invertible
hence H₂(G) is invertible by Th1; :: according to MONOID_0:def 16 :: thesis: verum