theorem :: MATGRP_0:97

for M being non empty right_unital left_unital associative multLoopStr holds UnitGroup M is strict Group ;