theorem :: RADIX_5:15

for n, k being Nat st n >= 1 & k >= 2 holds
for tx, ty, tz being Tuple of n,k -SD st ( for i being Nat holds
( not i in Seg n or ( DigA (tx,i) = DigA (tz,i) & DigA (ty,i) = 0 ) or ( DigA (ty,i) = DigA (tz,i) & DigA (tx,i) = 0 ) ) ) holds
(SDDec tz) + (SDDec (DecSD (0,n,k))) = (SDDec tx) + (SDDec ty)