consider cz being CR_coefficients of m;
set z = (Sum (u (#) cz)) mod (Product m);
take (Sum (u (#) cz)) mod (Product m) ; :: thesis: for c being CR_coefficients of m holds (Sum (u (#) cz)) mod (Product m) = (Sum (u (#) c)) mod (Product m)

now

let c be CR_coefficients of m; :: thesis: (Sum (u (#) cz)) mod (Product m) = (Sum (u (#) c)) mod (Product m)
Sum (u (#) c), Sum (u (#) cz) are_congruent_mod Product m by A, exnon;
hence (Sum (u (#) cz)) mod (Product m) = (Sum (u (#) c)) mod (Product m) by INT_3:12; :: thesis: verum

end;

hence for c being CR_coefficients of m holds (Sum (u (#) cz)) mod (Product m) = (Sum (u (#) c)) mod (Product m) ; :: thesis: verum