theorem Th16: :: UNIROOTS:16
for R being Skew-Field
for a, b being Element of R
for c, d being Element of (MultGroup R) st a = c & b = d holds
c * d = a * b