set S = { n where n is Nat : n divides (2 |^ n) + 1 } ;
deffunc H₃( Nat) -> set = 3 |^ $1;
consider f being ManySortedSet of NAT such that
A1: for i being Element of NAT holds f . i = H₃(i) from PBOOLE:sch 5();
set R = rng f;
A2: dom f = NAT by PARTFUN1:def 2;
A3: rng f c= { n where n is Nat : n divides (2 |^ n) + 1 }

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng f or x in { n where n is Nat : n divides (2 |^ n) + 1 } )
assume x in rng f ; :: thesis: x in { n where n is Nat : n divides (2 |^ n) + 1 }
then consider m being object such that
A4: m in dom f and
A5: x = f . m by FUNCT_1:def 3;
reconsider m = m as Element of NAT by A4, PARTFUN1:def 2;
A6: f . m = H₃(m) by A1;
3 |^ m divides (2 |^ (3 |^ m)) + 1 by Th37;
hence x in { n where n is Nat : n divides (2 |^ n) + 1 } by A5, A6; :: thesis: verum

end;

for m being Nat ex N being Nat st
( N >= m & N in rng f )

proof

let m be Nat; :: thesis: ex N being Nat st
( N >= m & N in rng f )
take n = H₃(m + 1); :: thesis: ( n >= m & n in rng f )
A7: m <= 3 |^ m by NEWTON:86;
m + 0 <= m + 1 by XREAL_1:6;
then 3 |^ m <= 3 |^ (m + 1) by NAT_6:1;
hence n >= m by A7, XXREAL_0:2; :: thesis: n in rng f
f . (m + 1) = n by A1;
hence n in rng f by A2, FUNCT_1:def 3; :: thesis: verum

end;

hence { n where n is Nat : n divides (2 |^ n) + 1 } is infinite by A3, PYTHTRIP:9; :: thesis: verum