theorem MG: :: FIELD_15:10

for R being Skew-Field
for n being Nat
for a being Element of R
for b being Element of (MultGroup R) st a = b holds
a |^ n = b |^ n