let a, b be Nat; :: thesis:
assume A1: ( a > 0 & a,b are_coprime ) ; :: thesis:
defpred S₁[ set ] means ( $1 is finite & not 0 in $1 & ( for n, m being Nat st n in $1 & m in $1 & n <> m holds
(ArProg (b,a)) . n,(ArProg (b,a)) . m are_coprime ) );
defpred S₂[ object , object ] means for Y being set st Y = $1 & S₁[Y] holds
ex k being Nat st
( not k in Y & $2 = Y \/ {k} & S₁[Y \/ {k}] );
A2: for x being object st x in bool NAT holds
ex y being object st
( y in bool NAT & S₂[x,y] )

let x be object ; :: thesis:
assume A3: x in bool NAT ; :: thesis:
reconsider N = x as set by A3;

suppose not S₁[N] ; :: thesis:

then S₂[N,N] ;
hence ex y being object st
( y in bool NAT & S₂[x,y] ) by A3; :: thesis:

end;

suppose A4: S₁[N] ; :: thesis:

then reconsider N = N as finite Subset of NAT by A3;
set C = canFS N;
defpred S₃[ object , object ] means $2 = (ArProg (b,a)) . ((canFS N) . $1);
A5: for k being Nat st k in Seg (len (canFS N)) holds
ex x being Element of NAT st S₃[k,x] ;
consider p being FinSequence of NAT such that
A6: dom p = Seg (len (canFS N)) and
A7: for k being Nat st k in Seg (len (canFS N)) holds
S₃[k,p . k] from FINSEQ_1:sch 5(A5);
A8: dom p = dom (canFS N) by A6, FINSEQ_1:def 3;
Product p <> 0

proof

assume Product p = 0 ; :: thesis:
then consider k being Nat such that
A9: ( k in dom p & p . k = 0 ) by RVSUM_1:103;
set Ck = (canFS N) . k;
( (canFS N) . k in rng (canFS N) & rng (canFS N) = N ) by A9, A8, FUNCT_1:def 3, FUNCT_2:def 3;
then (canFS N) . k <> 0 by A4;
then A10: b + (a * ((canFS N) . k)) <> 0 by A1;
p . k = (ArProg (b,a)) . ((canFS N) . k) by A9, A6, A7;
hence contradiction by A9, A10, NUMBER06:7; :: thesis:

end;

then reconsider m = Product p as non zero Nat ;
reconsider RC = (rng (ArProg (b,a))) /\ (Coprimes m) as infinite set by A1, NUMBER09:17;
RC \ ((rng p) \/ {b}) is infinite by RAMSEY_1:4;
then consider r being object such that
A11: r in RC \ ((rng p) \/ {b}) by XBOOLE_0:def 1;
r in rng (ArProg (b,a)) by A11, XBOOLE_0:def 4;
then consider k being object such that
A12: ( k in dom (ArProg (b,a)) & (ArProg (b,a)) . k = r ) by FUNCT_1:def 3;
reconsider r = r, k = k as Nat by A12;
set Nk = N \/ {k};
take N \/ {k} ; :: thesis:
N \/ {k} c= NAT by ORDINAL1:def 12, ZFMISC_1:137;
hence N \/ {k} in bool NAT ; :: thesis:
let XX be set ; :: thesis:
assume A13: ( XX = x & S₁[XX] ) ; :: thesis:
take k ; :: thesis:
thus not k in XX :: thesis:

proof

assume k in XX ; :: thesis:
then k in rng (canFS N) by A13, FUNCT_2:def 3;
then consider i being object such that
A14: ( i in dom (canFS N) & (canFS N) . i = k ) by FUNCT_1:def 3;
reconsider i = i as Nat by A14;
p . i = (ArProg (b,a)) . ((canFS N) . i) by A8, A14, A6, A7;
then r in rng p by A12, A8, A14, FUNCT_1:def 3;
then r in (rng p) \/ {b} by XBOOLE_0:def 3;
hence contradiction by A11, XBOOLE_0:def 5; :: thesis:

end;

thus N \/ {k} = XX \/ {k} by A13; :: thesis:
S₁[XX \/ {k}]

proof

thus XX \/ {k} is finite by A13; :: thesis:
thus not 0 in XX \/ {k} :: thesis:

proof

assume 0 in XX \/ {k} ; :: thesis:
then 0 = k by A13, ZFMISC_1:136;
then r = b + (a * 0) by A12, NUMBER06:7;
then r in (rng p) \/ {b} by ZFMISC_1:136;
hence contradiction by A11, XBOOLE_0:def 5; :: thesis:

end;

A15: for n being Nat st n in XX holds
(ArProg (b,a)) . n,(ArProg (b,a)) . k are_coprime

proof

let n be Nat; :: thesis:
assume n in XX ; :: thesis:
then n in rng (canFS N) by A13, FUNCT_2:def 3;
then consider i being object such that
A16: ( i in dom (canFS N) & (canFS N) . i = n ) by FUNCT_1:def 3;
reconsider i = i as Nat by A16;
A17: p . i = (ArProg (b,a)) . ((canFS N) . i) by A8, A16, A6, A7;
r in Coprimes m by A11, XBOOLE_0:def 4;
then r in { j where j is Integer : m,j are_coprime } by NUMBER09:def 2;
then ex j being Integer st
( r = j & m,j are_coprime ) ;
hence (ArProg (b,a)) . n,(ArProg (b,a)) . k are_coprime by A12, A16, A17, A8, INT_4:32, NUMBER12:4; :: thesis:

end;

let n, m be Nat; :: thesis:
assume A18: ( n in XX \/ {k} & m in XX \/ {k} & n <> m ) ; :: thesis:

per cases by A18, ZFMISC_1:136;

suppose ( n in XX & m in XX ) ; :: thesis:

hence (ArProg (b,a)) . n,(ArProg (b,a)) . m are_coprime by A18, A13; :: thesis:

end;

suppose ( ( n in XX & m = k ) or ( n = k & m in XX ) ) ; :: thesis:

hence (ArProg (b,a)) . n,(ArProg (b,a)) . m are_coprime by A15; :: thesis:

end;

suppose ( n = k & m = k ) ; :: thesis:

hence (ArProg (b,a)) . n,(ArProg (b,a)) . m are_coprime by A18; :: thesis:

end;

hence S₁[XX \/ {k}] ; :: thesis:

end;

consider g being Function such that
( dom g = bool NAT & rng g c= bool NAT ) and
A19: for x being object st x in bool NAT holds
S₂[x,g . x] from FUNCT_1:sch 6(A2);
deffunc H₁( object , object ) -> set = g . $2;
consider f being Function such that
A20: ( dom f = NAT & f . 0 = {} ) and
A21: for n being Nat holds f . (n + 1) = H₁(n,f . n) from NAT_1:sch 11();
defpred S₃[ Nat] means ( f . $1 is finite & f . $1 in bool NAT & S₁[f . $1] & ( for X being finite set st X = f . $1 holds
card X = $1 ) );
{} c= NAT ;
then A22: S₃[ 0 ] by A20;
A23: for n being Nat st S₃[n] holds
S₃[n + 1]

proof

let n be Nat; :: thesis:
assume A24: S₃[n] ; :: thesis:
then reconsider fn = f . n as finite Subset of NAT ;
A25: f . (n + 1) = g . fn by A21;
consider k being Nat such that
A26: ( not k in fn & g . fn = fn \/ {k} & S₁[fn \/ {k}] ) by A19, A24;
reconsider gfn = g . fn as finite set by A26;
A27: fn \/ {k} c= NAT by ORDINAL1:def 12, ZFMISC_1:137;
card fn = n by A24;
hence S₃[n + 1] by A27, A26, A25, CARD_2:41; :: thesis:

end;

A28: for n being Nat holds S₃[n] from NAT_1:sch 2(A22, A23);
A29: union (rng f) is infinite

proof

assume union (rng f) is finite ; :: thesis:
then reconsider U = union (rng f) as finite set ;
reconsider fC = f . ((card U) + 1) as finite set by A28;
fC in rng f by A20, FUNCT_1:def 3;
then ( (card U) + 1 = card fC & card fC <= card U ) by A28, NAT_1:43, ZFMISC_1:74;
hence contradiction by NAT_1:13; :: thesis:

end;

union (rng f) c= NAT

proof

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume y in union (rng f) ; :: thesis:
then consider Y being set such that
A30: ( y in Y & Y in rng f ) by TARSKI:def 4;
consider x being object such that
A31: ( x in dom f & f . x = Y ) by A30, FUNCT_1:def 3;
reconsider x = x as Nat by A20, A31;
f . x in bool NAT by A28;
hence y in NAT by A30, A31; :: thesis:

end;

then reconsider N = union (rng f) as infinite Subset of NAT by A29;
take N ; :: thesis:
defpred S₄[ Nat] means for n being Nat holds f . n c= f . (n + $1);
A32: S₄[ 0 ] ;
A33: for k being Nat st S₄[k] holds
S₄[k + 1]

proof

let k be Nat; :: thesis:
assume A34: S₄[k] ; :: thesis:
let n be Nat; :: thesis:
A35: f . n c= f . (n + k) by A34;
A36: f . ((n + k) + 1) = g . (f . (n + k)) by A21;
( f . (n + k) in bool NAT & S₁[f . (n + k)] ) by A28;
then consider l being Nat such that
A37: ( not l in f . (n + k) & g . (f . (n + k)) = (f . (n + k)) \/ {l} & S₁[(f . (n + k)) \/ {l}] ) by A19;
f . (n + k) c= f . ((n + k) + 1) by A36, A37, XBOOLE_1:7;
hence f . n c= f . (n + (k + 1)) by A35, XBOOLE_1:1; :: thesis:

end;

A38: for n being Nat holds S₄[n] from NAT_1:sch 2(A32, A33);
let n, m be Nat; :: thesis:
assume A39: ( n in N & m in N & n <> m ) ; :: thesis:
consider N being set such that
A40: ( n in N & N in rng f ) by A39, TARSKI:def 4;
consider xn being object such that
A41: ( xn in dom f & f . xn = N ) by A40, FUNCT_1:def 3;
consider M being set such that
A42: ( m in M & M in rng f ) by A39, TARSKI:def 4;
consider xm being object such that
A43: ( xm in dom f & f . xm = M ) by A42, FUNCT_1:def 3;
reconsider xn = xn, xm = xm as Nat by A20, A41, A43;
( f . xn c= f . (xn + xm) & f . xm c= f . (xn + xm) ) by A38;
hence (ArProg (b,a)) . n,(ArProg (b,a)) . m are_coprime by A40, A41, A42, A43, A28, A39; :: thesis: