let u be integer-valued FinSequence; :: thesis: for m being CR_Sequence st dom u = dom m holds
{ z where z is positive Nat : z solves_CRT u,m } is infinite
let m be CR_Sequence; :: thesis: ( dom u = dom m implies { z where z is positive Nat : z solves_CRT u,m } is infinite )
assume A1: dom u = dom m ; :: thesis: { z where z is positive Nat : z solves_CRT u,m } is infinite
set X = { x where x is positive Nat : x solves_CRT u,m } ;
CRT (u,m) solves_CRT u,m by A1, Def4;
then (CRT (u,m)) + (1 * (Product m)) solves_CRT u,m by A1, Th30;
then A2: (CRT (u,m)) + (1 * (Product m)) in { x where x is positive Nat : x solves_CRT u,m } ;
A3: { x where x is positive Nat : x solves_CRT u,m } is natural-membered

proof

let a be object ; :: according to MEMBERED:def 6 :: thesis: ( not a in { x where x is positive Nat : x solves_CRT u,m } or a is natural )
assume a in { x where x is positive Nat : x solves_CRT u,m } ; :: thesis: a is natural
then ex x being positive Nat st
( a = x & x solves_CRT u,m ) ;
hence a is natural ; :: thesis: verum

end;

for a being Nat st a in { x where x is positive Nat : x solves_CRT u,m } holds
ex b being Nat st
( b > a & b in { x where x is positive Nat : x solves_CRT u,m } )

proof

let a be Nat; :: thesis: ( a in { x where x is positive Nat : x solves_CRT u,m } implies ex b being Nat st
( b > a & b in { x where x is positive Nat : x solves_CRT u,m } ) )
assume a in { x where x is positive Nat : x solves_CRT u,m } ; :: thesis: ex b being Nat st
( b > a & b in { x where x is positive Nat : x solves_CRT u,m } )
then consider x being positive Nat such that
A4: a = x and
A5: x solves_CRT u,m ;
take b = x + (1 * (Product m)); :: thesis: ( b > a & b in { x where x is positive Nat : x solves_CRT u,m } )
x + (Product m) > x + 0 by XREAL_1:8;
hence b > a by A4; :: thesis: b in { x where x is positive Nat : x solves_CRT u,m }
b solves_CRT u,m by A1, A5, Th30;
hence b in { x where x is positive Nat : x solves_CRT u,m } ; :: thesis: verum

end;

hence { z where z is positive Nat : z solves_CRT u,m } is infinite by A2, A3, NUMBER04:1; :: thesis: verum