let a be Nat; :: thesis: for k, l being Integer st k,l are_relative_prime holds
k |^ a,l are_relative_prime
let k, l be Integer; :: thesis: ( k,l are_relative_prime implies k |^ a,l are_relative_prime )
defpred S₁[ Nat] means k |^ $1,l are_relative_prime ;
assume A1: k,l are_relative_prime ; :: thesis: k |^ a,l are_relative_prime
A2: for a being Nat st S₁[a] holds
S₁[a + 1]

proof

let a be Nat; :: thesis: ( S₁[a] implies S₁[a + 1] )
assume k |^ a,l are_relative_prime ; :: thesis: S₁[a + 1]
then k * (k |^ a),l are_relative_prime by A1, INT_2:41;
hence S₁[a + 1] by NEWTON:11; :: thesis: verum

end;

k |^ 0 = 1 by NEWTON:9;
then A3: S₁[ 0 ] by Th14;
for a being Nat holds S₁[a] from NAT_1:sch 2(A3, A2);
hence k |^ a,l are_relative_prime ; :: thesis: verum