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