let n, k be Nat; :: thesis: ( n >= 1 & k >= 2 implies 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) )
assume A1: ( n >= 1 & k >= 2 ) ; :: thesis: 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)
let tx, ty, tz be Tuple of n,(k -SD ); :: thesis: ( ( 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 ) ) ) implies (SDDec tz) + (SDDec (DecSD 0 ,n,k)) = (SDDec tx) + (SDDec ty) )
assume A2: 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 ) ) ; :: thesis: (SDDec tz) + (SDDec (DecSD 0 ,n,k)) = (SDDec tx) + (SDDec ty)
for i being Nat holds
( not i in Seg n or ( DigA tx,i = DigA tz,i & DigA ty,i = DigA (DecSD 0 ,n,k),i ) or ( DigA ty,i = DigA tz,i & DigA tx,i = DigA (DecSD 0 ,n,k),i ) )

proof

let i be Nat; :: thesis: ( not i in Seg n or ( DigA tx,i = DigA tz,i & DigA ty,i = DigA (DecSD 0 ,n,k),i ) or ( DigA ty,i = DigA tz,i & DigA tx,i = DigA (DecSD 0 ,n,k),i ) )
assume A3: i in Seg n ; :: thesis: ( ( DigA tx,i = DigA tz,i & DigA ty,i = DigA (DecSD 0 ,n,k),i ) or ( DigA ty,i = DigA tz,i & DigA tx,i = DigA (DecSD 0 ,n,k),i ) )
then DigA (DecSD 0 ,n,k),i = 0 by Th5;
hence ( ( DigA tx,i = DigA tz,i & DigA ty,i = DigA (DecSD 0 ,n,k),i ) or ( DigA ty,i = DigA tz,i & DigA tx,i = DigA (DecSD 0 ,n,k),i ) ) by A2, A3; :: thesis: verum

end;

hence (SDDec tz) + (SDDec (DecSD 0 ,n,k)) = (SDDec tx) + (SDDec ty) by A1, Th14; :: thesis: verum