theorem Th31: :: INT_6:31

for u being INT -valued FinSequence
for m being CR_Sequence st len m = len u holds
( 0 <= to_int (u,m) & to_int (u,m) < Product m )