theorem Th12: :: WSIERP_1:12

for a, b being Nat
for k, l being Integer st k gcd l = 1 holds
( k gcd (l |^ b) = 1 & (k |^ a) gcd (l |^ b) = 1 )