:: deftheorem defines solves_CRT NUMBER14:def 3 :
for u, m being integer-valued FinSequence
for z being Integer holds
( z solves_CRT u,m iff for i being Nat st i in dom u holds
z,u . i are_congruent_mod m . i );