let u be integer-valued FinSequence; :: thesis: for m being CR_Sequence st dom u = dom m holds
{ z where z is Nat : z solves_CRT u,m } is infinite
let m be CR_Sequence; :: thesis: ( dom u = dom m implies { z where z is Nat : z solves_CRT u,m } is infinite )
set X = { x where x is positive Nat : x solves_CRT u,m } ;
{ x where x is positive Nat : x solves_CRT u,m } c= { x where x is Nat : x solves_CRT u,m }

proof

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

end;

hence ( dom u = dom m implies { z where z is Nat : z solves_CRT u,m } is infinite ) by Th31; :: thesis: verum