theorem Th9: :: RADIX_2:9

for k, n being Nat
for x being Tuple of n + 1,k -SD
for xn being Tuple of n,k -SD st ( for i being Nat st i in Seg n holds
x . i = xn . i ) holds
Sum (DigitSD x) = Sum ((DigitSD xn) ^ <*(SubDigit (x,(n + 1),k))*>)