A1: PrimeNumbersFS s = Sgm (rng (PrimeNumbersFS s)) by MATRIX15:6;
rng (PrimeNumbersFS s) is Subset of SetPrimes by RELAT_1:def 19;
hence PrimeNumbersFS s is Chinese_Remainder by A1; :: thesis: verum