let a be Nat; :: thesis: for k, l being Integer st k,l are_coprime holds
k |^ a,l are_coprime
let k, l be Integer; :: thesis: ( k,l are_coprime implies k |^ a,l are_coprime )
defpred S1[ Nat] means k |^ $1,l are_coprime ;
assume A1: k,l are_coprime ; :: thesis: k |^ a,l are_coprime
A2: for a being Nat st S1[a] holds
S1[a + 1]
proof
let a be Nat; :: thesis: ( S1[a] implies S1[a + 1] )
assume k |^ a,l are_coprime ; :: thesis: S1[a + 1]
then k * (k |^ a),l are_coprime by A1, INT_2:26;
hence S1[a + 1] by NEWTON:6; :: thesis: verum
end;
k |^ 0 = 1 by NEWTON:4;
then A3: S1[ 0 ] by Th9;
for a being Nat holds S1[a] from NAT_1:sch 2(A3, A2);
 hence k |^ a,l are_coprime ; :: thesis: verum