let a, m be Nat; :: thesis: ( a <> 0 & m <> 0 & a,m are_coprime implies for b being Nat holds a |^ b,m are_coprime )
defpred S₁[ Nat] means a |^ $1,m are_coprime ;
assume A1: ( a <> 0 & m <> 0 & a,m are_coprime ) ; :: thesis: for b being Nat holds a |^ b,m are_coprime
A2: for b being Nat st S₁[b] holds
S₁[b + 1]

proof

let b be Nat; :: thesis: ( S₁[b] implies S₁[b + 1] )
a |^ (b + 1) = (a |^ b) * (a |^ 1) by NEWTON:8
.= (a |^ b) * a ;
hence ( S₁[b] implies S₁[b + 1] ) by A1, EULER_1:14; :: thesis: verum

end;

( (a |^ 0) gcd m = 1 gcd m & m gcd 1 = 1 ) by NEWTON:4, NEWTON:51;
then A4: S₁[ 0 ] by INT_2:def 3;
for b being Nat holds S₁[b] from NAT_1:sch 2(A4, A2);
hence for b being Nat holds a |^ b,m are_coprime ; :: thesis: verum