set c = the CR_coefficients of m;
let z1, z2 be Integer; :: thesis: ( ( for c being CR_coefficients of m holds z1 = (Sum (u (#) c)) mod (Product m) ) & ( for c being CR_coefficients of m holds z2 = (Sum (u (#) c)) mod (Product m) ) implies z1 = z2 )
assume A2: for c being CR_coefficients of m holds z1 = (Sum (u (#) c)) mod (Product m) ; :: thesis: ( ex c being CR_coefficients of m st not z2 = (Sum (u (#) c)) mod (Product m) or z1 = z2 )
assume A3: for c being CR_coefficients of m holds z2 = (Sum (u (#) c)) mod (Product m) ; :: thesis: z1 = z2
thus z1 = (Sum (u (#) the CR_coefficients of m)) mod (Product m) by A2
.= z2 by A3 ; :: thesis: verum