for R being Skew-Field
for x being Element of (MultGroup R)
for y being Element of R st y = x holds
for k being Nat holds (power (MultGroup R)) . (x,k) = (power R) . (y,k)