len u = len m
by A1, FINSEQ_3:29;
then consider z being Integer such that
A2:
0 <= z
and
A3:
( z < Product m & ( for i being Nat st i in dom u holds
z,u . i are_congruent_mod m . i ) )
by INT_6:41;
reconsider z = z as Element of NAT by A2, INT_1:3;
take
z
; ( z solves_CRT u,m & z < Product m )
thus
( z solves_CRT u,m & z < Product m )
by A3; verum