let G be non empty right_unital left_unital associative multLoopStr ; :: thesis: ( G is Group-like implies UnitGroup G = multMagma(# the carrier of G, the multF of G #) )
assume G is Group-like ; :: thesis: UnitGroup G = multMagma(# the carrier of G, the multF of G #)
then units G = the carrier of G by Th114;
hence UnitGroup G = multMagma(# the carrier of G, the multF of G #) ; :: thesis: verum