for a, b, k, l being Nat st l > 0 holds
ex x being Nat st ((a,b) In_Power (k + l)) . l = a * x