theorem Th3: :: HURWITZ:3

for L being non empty well-unital associative multLoopStr
for x being Element of L
for k1, k2 being Element of NAT holds ((power L) . (x,k1)) * ((power L) . (x,k2)) = (power L) . (x,(k1 + k2))