let z be non zero Nat; :: thesis: { k where k is Nat : ( k is odd & (2 |^ (2 |^ z)) + k is composite ) } is infinite
set S = { k where k is Nat : ( k is odd & (2 |^ (2 |^ z)) + k is composite ) } ;
deffunc H₁( Nat) -> set = (6 * $1) - 1;
consider f being ManySortedSet of NATPLUS such that
A1: for n being Element of NATPLUS holds f . n = H₁(n) from PBOOLE:sch 5();
set R = rng f;
A2: dom f = NATPLUS by PARTFUN1:def 2;
A3: rng f c= { k where k is Nat : ( k is odd & (2 |^ (2 |^ z)) + k is composite ) }

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in rng f or a in { k where k is Nat : ( k is odd & (2 |^ (2 |^ z)) + k is composite ) } )
assume a in rng f ; :: thesis: a in { k where k is Nat : ( k is odd & (2 |^ (2 |^ z)) + k is composite ) }
then consider t being object such that
A4: t in dom f and
A5: a = f . t by FUNCT_1:def 3;
reconsider t = t as Element of NATPLUS by A4, PARTFUN1:def 2;
A6: a = (6 * t) - 1 by A1, A5;
A7: (2 * (3 * t)) - 1 is odd ;
0 + 1 <= t by NAT_1:13;
then (2 |^ (2 |^ z)) + ((6 * t) - 1) is composite by Th64;
hence a in { k where k is Nat : ( k is odd & (2 |^ (2 |^ z)) + k is composite ) } by A6, A7; :: 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 )
1 * m <= 6 * m by XREAL_1:64;
then A8: m + 0 <= (6 * m) + 5 by XREAL_1:7;
reconsider n = H₁(m + 1) as Element of NAT by INT_1:3;
take n ; :: thesis: ( n >= m & n in rng f )
thus n >= m by A8; :: thesis: n in rng f
A9: m + 1 in NATPLUS by NAT_LAT:def 6;
then f . (m + 1) = n by A1;
hence n in rng f by A2, A9, FUNCT_1:def 3; :: thesis: verum

end;

hence { k where k is Nat : ( k is odd & (2 |^ (2 |^ z)) + k is composite ) } is infinite by A3, PYTHTRIP:9; :: thesis: verum