let u be INT -valued FinSequence; :: thesis: for m being CR_Sequence st len m = len u holds
( 0 <= to_int (u,m) & to_int (u,m) < Product m )
let m be CR_Sequence; :: thesis: ( len m = len u implies ( 0 <= to_int (u,m) & to_int (u,m) < Product m ) )
set z = to_int (u,m);
set c = the CR_coefficients of m;
assume len u = len m ; :: thesis: ( 0 <= to_int (u,m) & to_int (u,m) < Product m )
then to_int (u,m) = (Sum (u (#) the CR_coefficients of m)) mod (Product m) by Def5;
hence ( 0 <= to_int (u,m) & to_int (u,m) < Product m ) by NAT_D:62; :: thesis: verum