defpred S₁[ Nat] means ex k being Nat st
( k = (10 |^ ((2 * $1) + 1)) + 1 & 11 divides k );
let n, k be Nat; :: thesis: ( k = (10 |^ ((2 * n) + 1)) + 1 implies 11 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 |^ ((2 * k) + 1)) + 1 and
A3: 11 divides l ;
consider m being Nat such that
A4: l = 11 * m by A3, NAT_D:def 3;
(10 |^ ((2 * (k + 1)) + 1)) + 1 = (10 |^ (((2 * k) + 1) + 2)) + 1
.= (((11 * m) - 1) * (10 |^ (1 + 1))) + 1 by A2, A4, NEWTON:8
.= (((11 * m) - 1) * ((10 |^ 1) * 10)) + 1 by NEWTON:6
.= (((11 * m) - 1) * (10 * 10)) + 1
.= 11 * ((m * 100) - 9) ;
hence S₁[k + 1] by INT_1:def 3; :: thesis: verum

end;

A5: S₁[ 0 ] ;
for k being Nat holds S₁[k] from NAT_1:sch 2(A5, A1);
then A6: ex l being Nat st
( l = (10 |^ ((2 * n) + 1)) + 1 & 11 divides l ) ;
assume k = (10 |^ ((2 * n) + 1)) + 1 ; :: thesis: 11 divides k
hence 11 divides k by A6; :: thesis: verum