theorem Th14: :: RADIX_5:14

for n being Nat st n >= 1 holds
for k being Nat st k >= 2 holds
for tx, ty, tz, tw 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) = DigA (tw,i) ) or ( DigA (ty,i) = DigA (tz,i) & DigA (tx,i) = DigA (tw,i) ) ) ) holds
(SDDec tz) + (SDDec tw) = (SDDec tx) + (SDDec ty)