consider m1, m2 being Integer such that
A4: n1 gcd n2 = (m1 * n1) + (m2 * n2) by NAT_D:68;
set x = ((a1 * m2) * n2) + ((a2 * m1) * n1);
reconsider y = (((a1 * m2) * n2) + ((a2 * m1) * n1)) mod (n1 * n2) as Element of NAT by INT_1:3, INT_1:57;
take y ; :: thesis: ( y solves_CRT a1,n1,a2,n2 & y < n1 * n2 )
((a1 * m2) * n2) + ((a2 * m1) * n1) solves_CRT a1,n1,a2,n2

proof

((a1 * m2) * n2) + ((a2 * m1) * n1) = (a1 * (m2 * n2)) + ((a2 * m1) * n1)
.= (a1 * (1 - (m1 * n1))) + ((a2 * m1) * n1) by A1, A4
.= a1 + (((a2 - a1) * m1) * n1) ;
hence ((a1 * m2) * n2) + ((a2 * m1) * n1),a1 are_congruent_mod n1 ; :: according to NUMBER14:def 1 :: thesis: ((a1 * m2) * n2) + ((a2 * m1) * n1),a2 are_congruent_mod n2
((a1 * m2) * n2) + ((a2 * m1) * n1) = (a2 * (m1 * n1)) + ((a1 * m2) * n2)
.= (a2 * (1 - (m2 * n2))) + ((a1 * m2) * n2) by A1, A4
.= a2 + (((a1 - a2) * m2) * n2) ;
hence ((a1 * m2) * n2) + ((a2 * m1) * n1),a2 are_congruent_mod n2 ; :: thesis: verum

end;

hence y solves_CRT a1,n1,a2,n2 by A2, A3, Th27; :: thesis: y < n1 * n2
thus y < n1 * n2 by A2, A3, INT_1:58; :: thesis: verum