set cz = the CR_coefficients of m;
take z = (Sum (u (#) the CR_coefficients of m)) mod (Product m); :: thesis: for c being CR_coefficients of m holds z = (Sum (u (#) c)) mod (Product m)
for c being CR_coefficients of m holds z = (Sum (u (#) c)) mod (Product m) by NAT_D:64, A1, Th30;
hence for c being CR_coefficients of m holds z = (Sum (u (#) c)) mod (Product m) ; :: thesis: verum