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