let n, k be Nat; :: thesis: ( k = (10 |^ n) - 1 implies 9 divides k )
assume A1: k = (10 |^ n) - 1 ; :: thesis: 9 divides k
defpred S₁[ Nat] means ex k being Nat st
( k = (10 |^ $1) - 1 & 9 divides k );
A2: (10 |^ 0 ) - 1 = 1 - 1 by NEWTON:9
.= 0 ;
A3: S₁[ 0 ] by A2, NAT_D:6;

A4: now

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
A5: ( l = (10 |^ k) - 1 & 9 divides l ) ;
consider m being Nat such that
A6: l = 9 * m by A5, NAT_D:def 3;
A7: (10 |^ (k + 1)) - 1 = (((9 * m) + 1) * 10) - 1 by A5, A6, NEWTON:11
.= 9 * ((m * 10) + 1) ;
9 divides 9 * ((m * 10) + 1) by NAT_D:def 3;
hence S₁[k + 1] by A7; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A3, A4);
then consider l being Nat such that
A8: ( l = (10 |^ n) - 1 & 9 divides l ) ;
thus 9 divides k by A1, A8; :: thesis: verum