:: deftheorem Def6 defines SD2SDSubDigit RADIX_3:def 6 :
for i, k, n being Nat
for x being Tuple of n,k -SD holds
( ( i in Seg n implies SD2SDSubDigit (x,i,k) = (SDSub_Add_Data ((DigA (x,i)),k)) + (SDSub_Add_Carry ((DigA (x,(i -' 1))),k)) ) & ( i = n + 1 implies SD2SDSubDigit (x,i,k) = SDSub_Add_Carry ((DigA (x,(i -' 1))),k) ) & ( not i in Seg n & not i = n + 1 implies SD2SDSubDigit (x,i,k) = 0 ) );