let a, m be Nat; :: thesis: ( a <> 0 & m <> 0 & a,m are_relative_prime implies for b being Nat holds a |^ b,m are_relative_prime )
assume A1: ( a <> 0 & m <> 0 & a,m are_relative_prime ) ; :: thesis: for b being Nat holds a |^ b,m are_relative_prime
A2: (a |^ 0 ) gcd m = 1 gcd m by NEWTON:9;
defpred S₁[ Nat] means a |^ $1,m are_relative_prime ;
m gcd 1 = 1 by NEWTON:64;
then A3: S₁[ 0 ] by A2, INT_2:def 4;
A4: for b being Nat st S₁[b] holds
S₁[b + 1]

proof

let b be Nat; :: thesis: ( S₁[b] implies S₁[b + 1] )
assume A5: a |^ b,m are_relative_prime ; :: thesis: S₁[b + 1]
A6: a |^ (b + 1) = (a |^ b) * (a |^ 1) by NEWTON:13
.= (a |^ b) * a by NEWTON:10 ;
a |^ b <> 0 by A1, PREPOWER:12;
hence S₁[b + 1] by A1, A5, A6, EULER_1:15; :: thesis: verum

end;

for b being Nat holds S₁[b] from NAT_1:sch 2(A3, A4);
hence for b being Nat holds a |^ b,m are_relative_prime ; :: thesis: verum