theorem Th110: :: MATGRP_0:95

for M being non empty right_unital associative multLoopStr
for a, b being Element of M
for x, y being Element of (UnitGroup M) st a = x & b = y holds
a * b = x * y by FUNCT_1:49, ZFMISC_1:87;