let u be integer-yielding 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 ) )
assume AS: len u = len m ; :: thesis: ( 0 <= to_int u,m & to_int u,m < Product m )
set z = to_int u,m;
consider c being CR_coefficients of m;
to_int u,m = (Sum (u (#) c)) mod (Product m) by AS, Df5;
hence ( 0 <= to_int u,m & to_int u,m < Product m ) by INT_3:9; :: thesis: verum