deffunc H1( object , Nat) -> Element of NAT = In ((primenumber ($2 !)),NAT);
consider f being sequence of NAT such that
A1: ( f . 0 = 7 & ( for k being Nat holds f . (k + 1) = H1(k,f . k) ) ) from NAT_1:sch 12();
 defpred S1[ Nat] means ( f . $1 is Prime & 5 < f . $1 );
A2: S1[ 0 ] by A1, NAT_4:26;
A3: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume A4: S1[n] ; :: thesis: S1[n + 1]
A5: f . (n + 1) = In ((primenumber ((f . n) !)),NAT) by A1
.= primenumber ((f . n) !) ;
( f . n <= (f . n) ! & (f . n) ! <= primenumber ((f . n) !) ) by PRIMRECI:11, NEWTON:38;
then f . n <= f . (n + 1) by A5, XXREAL_0:2;
hence S1[n + 1] by A4, A5, XXREAL_0:2; :: thesis: verum
end;
A6: for n being Nat holds S1[n] from NAT_1:sch 2(A2, A3);
 A7: for i, j being Nat st i <= j holds
f . i <= f . j
proof
let i be Nat; :: thesis: for j being Nat st i <= j holds
f . i <= f . j
defpred S2[ Nat] means f . i <= f . (i + $1);
A8: S2[ 0 ] ;
A9: for j being Nat st S2[j] holds
S2[j + 1]
proof
let j be Nat; :: thesis: ( S2[j] implies S2[j + 1] )
assume A10: S2[j] ; :: thesis: S2[j + 1]
f . ((i + j) + 1) = In ((primenumber ((f . (i + j)) !)),NAT) by A1
.= primenumber ((f . (i + j)) !) ;
then ( f . (i + j) <= (f . (i + j)) ! & (f . (i + j)) ! <= f . ((i + j) + 1) ) by PRIMRECI:11, NEWTON:38;
then f . (i + j) <= f . ((i + j) + 1) by XXREAL_0:2;
hence S2[j + 1] by A10, XXREAL_0:2; :: thesis: verum
end;
A11: for j being Nat holds S2[j] from NAT_1:sch 2(A8, A9);
 let j be Nat; :: thesis: ( i <= j implies f . i <= f . j )
assume i <= j ; :: thesis: f . i <= f . j
then reconsider ji = j - i as Nat by NAT_1:21;
S2[ji] by A11;
hence f . i <= f . j ; :: thesis: verum
end;
defpred S2[ object , object ] means ( $2 is Prime & ( for i, j being Nat st $1 = i & $2 = j holds
( j is prime & f . i < j & j divides (((f . i) -' 1) !) + 1 ) ) );
A12: for x being object st x in NAT holds
ex y being object st
( y in NAT & S2[x,y] )
proof
let x be object ; :: thesis: ( x in NAT implies ex y being object st
( y in NAT & S2[x,y] ) )
assume A13: x in NAT ; :: thesis: ex y being object st
( y in NAT & S2[x,y] )
reconsider i = x as Nat by A13;
S1[i] by A6;
then consider q being Prime such that
A14: ( f . i < q & q divides (((f . i) -' 1) !) + 1 ) by Th24;
take q ; :: thesis: ( q in NAT & S2[x,q] )
thus ( q in NAT & S2[x,q] ) by A14, ORDINAL1:def 12; :: thesis: verum
end;
consider F being Function such that
A15: ( dom F = NAT & rng F c= NAT ) and
A16: for x being object st x in NAT holds
S2[x,F . x] from FUNCT_1:sch 6(A12);
 A17: for x1, x2 being object st x1 in dom F & x2 in dom F & F . x1 = F . x2 holds
x1 = x2
proof
let x1, x2 be object ; :: thesis: ( x1 in dom F & x2 in dom F & F . x1 = F . x2 implies x1 = x2 )
assume A18: ( x1 in dom F & x2 in dom F & F . x1 = F . x2 ) ; :: thesis: x1 = x2
reconsider x1 = x1, x2 = x2 as Element of NAT by A15, A18;
A19: ( S2[x1,F . x1] & S2[x2,F . x2] ) by A16;
reconsider Fx1 = F . x1, Fx2 = F . x2 as Prime by A16;
per cases ( x1 = x2 or x1 < x2 or x2 < x1 ) by XXREAL_0:1;
suppose x1 = x2 ; :: thesis: x1 = x2
hence x1 = x2 ; :: thesis: verum
end;
suppose x1 < x2 ; :: thesis: x1 = x2
then x1 + 1 <= x2 by NAT_1:13;
then A20: f . (x1 + 1) <= f . x2 by A7;
Fx1 divides (((f . x1) -' 1) !) + 1 by A16;
then A21: Fx1 <= (((f . x1) -' 1) !) + 1 by NAT_D:7;
1 < f . x1 by A6, XXREAL_0:2;
then ( (f . x1) -' 1 < ((f . x1) -' 1) + 1 & (f . x1) -' 1 = (f . x1) - 1 & (f . x1) - 1 > 1 - 1 ) by NAT_1:13, XREAL_1:233, XREAL_1:14;
then ( (((f . x1) -' 1) !) + 1 <= (f . x1) ! & (f . x1) ! <= primenumber ((f . x1) !) ) by Th25, NAT_1:13, PRIMRECI:11;
then ( (((f . x1) -' 1) !) + 1 <= primenumber ((f . x1) !) & primenumber ((f . x1) !) = In ((primenumber ((f . x1) !)),NAT) ) by XXREAL_0:2;
then (((f . x1) -' 1) !) + 1 <= f . (x1 + 1) by A1;
then (((f . x1) -' 1) !) + 1 <= f . x2 by A20, XXREAL_0:2;
hence x1 = x2 by A18, A21, A19, XXREAL_0:2; :: thesis: verum
end;
suppose x2 < x1 ; :: thesis: x1 = x2
then x2 + 1 <= x1 by NAT_1:13;
then A22: f . (x2 + 1) <= f . x1 by A7;
Fx2 divides (((f . x2) -' 1) !) + 1 by A16;
then A23: Fx2 <= (((f . x2) -' 1) !) + 1 by NAT_D:7;
1 < f . x2 by A6, XXREAL_0:2;
then ( (f . x2) -' 1 < ((f . x2) -' 1) + 1 & (f . x2) -' 1 = (f . x2) - 1 & (f . x2) - 1 > 1 - 1 ) by NAT_1:13, XREAL_1:14, XREAL_1:233;
then ( (((f . x2) -' 1) !) + 1 <= (f . x2) ! & (f . x2) ! <= primenumber ((f . x2) !) ) by Th25, NAT_1:13, PRIMRECI:11;
then ( (((f . x2) -' 1) !) + 1 <= primenumber ((f . x2) !) & primenumber ((f . x2) !) = In ((primenumber ((f . x2) !)),NAT) ) by XXREAL_0:2;
then (((f . x2) -' 1) !) + 1 <= f . (x2 + 1) by A1;
then (((f . x2) -' 1) !) + 1 <= f . x1 by A22, XXREAL_0:2;
hence x1 = x2 by A18, A23, A19, XXREAL_0:2; :: thesis: verum
end;
end;
end;
rng F c= { q where q is Prime : ex p being Prime st
( p < q & q divides ((p -' 1) !) + 1 ) }
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng F or y in { q where q is Prime : ex p being Prime st
( p < q & q divides ((p -' 1) !) + 1 ) } )
assume y in rng F ; :: thesis: y in { q where q is Prime : ex p being Prime st
( p < q & q divides ((p -' 1) !) + 1 ) }
then consider x being object such that
A24: ( x in dom F & F . x = y ) by FUNCT_1:def 3;
reconsider x = x as Nat by A15, A24;
reconsider Fx = F . x as Prime by A24, A15, A16;
A25: f . x is prime by A6;
( f . x < Fx & Fx divides (((f . x) -' 1) !) + 1 ) by A24, A15, A16;
hence y in { q where q is Prime : ex p being Prime st
( p < q & q divides ((p -' 1) !) + 1 ) } by A24, A25; :: thesis: verum
end;
hence { q where q is Prime : ex p being Prime st
( p < q & q divides ((p -' 1) !) + 1 ) } is infinite by A17, FUNCT_1:def 4, A15, CARD_1:59; :: thesis: verum