defpred S₁[ Nat] means ex k being Nat st
( k = (10 |^ $1) - 1 & 9 divides k );
let n, k be Nat; :: thesis: ( k = (10 |^ n) - 1 implies 9 divides k )

A1: now :: thesis: for k being Nat st S₁[k] holds
S₁[k + 1]

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume S₁[k] ; :: thesis: S₁[k + 1]
then consider l being Nat such that
A2: l = (10 |^ k) - 1 and
A3: 9 divides l ;
consider m being Nat such that
A4: l = 9 * m by A3, NAT_D:def 3;
A5: 9 divides 9 * ((m * 10) + 1) by NAT_D:def 3;
(10 |^ (k + 1)) - 1 = (((9 * m) + 1) * 10) - 1 by A2, A4, NEWTON:6
.= 9 * ((m * 10) + 1) ;
hence S₁[k + 1] by A5; :: thesis: verum

end;

(10 |^ 0) - 1 = 1 - 1 by NEWTON:4
.= 0 ;
then A6: S₁[ 0 ] by NAT_D:6;
for k being Nat holds S₁[k] from NAT_1:sch 2(A6, A1);
then A7: ex l being Nat st
( l = (10 |^ n) - 1 & 9 divides l ) ;
assume k = (10 |^ n) - 1 ; :: thesis: 9 divides k
hence 9 divides k by A7; :: thesis: verum