let G be non empty multMagma ; :: thesis: ( G is associative & G is invertible implies ( G is unital & G is cancelable ) )
assume ( G is associative & G is invertible ) ; :: thesis: ( G is unital & G is cancelable )
then reconsider G = G as non empty associative invertible multMagma ;
for a, b, c being Element of G st ( a * b = a * c or b * a = c * a ) holds
b = c by GROUP_1:6;
hence ( G is unital & G is cancelable ) by Th13; :: thesis: verum