let a1, n1, a2, n2 be Integer; :: thesis: for x being Integer st x solves_CRT a1,n1,a2,n2 holds
for k being Integer holds x + ((k * n1) * n2) solves_CRT a1,n1,a2,n2
let x be Integer; :: thesis: ( x solves_CRT a1,n1,a2,n2 implies for k being Integer holds x + ((k * n1) * n2) solves_CRT a1,n1,a2,n2 )
assume A1: x solves_CRT a1,n1,a2,n2 ; :: thesis: for k being Integer holds x + ((k * n1) * n2) solves_CRT a1,n1,a2,n2
let k be Integer; :: thesis: x + ((k * n1) * n2) solves_CRT a1,n1,a2,n2
set y = x + ((k * n1) * n2);
(k * n2) * n1, 0 are_congruent_mod n1 ;
then x + ((k * n1) * n2),a1 + 0 are_congruent_mod n1 by A1, INT_1:16;
hence x + ((k * n1) * n2),a1 are_congruent_mod n1 ; :: according to NUMBER14:def 1 :: thesis: x + ((k * n1) * n2),a2 are_congruent_mod n2
(k * n1) * n2, 0 are_congruent_mod n2 ;
then x + ((k * n1) * n2),a2 + 0 are_congruent_mod n2 by A1, INT_1:16;
hence x + ((k * n1) * n2),a2 are_congruent_mod n2 ; :: thesis: verum