theorem Th13: :: RADIX_3:13

for k being Nat
for i1 being Integer st 2 <= k & i1 in k -SD holds
( SDSub_Add_Data (i1,k) >= - (Radix (k -' 1)) & SDSub_Add_Data (i1,k) <= (Radix (k -' 1)) - 1 )