let n, k be Nat; :: thesis: for x being Tuple of n, NAT
for y being Tuple of n,k -SD st x = y holds
SDDec2 (x,k) = SDDec y
let x be Tuple of n, NAT ; :: thesis: for y being Tuple of n,k -SD st x = y holds
SDDec2 (x,k) = SDDec y
let y be Tuple of n,k -SD ; :: thesis: ( x = y implies SDDec2 (x,k) = SDDec y )
assume x = y ; :: thesis: SDDec2 (x,k) = SDDec y
then SDDec2 (x,k) = Sum (DigitSD y) by Th12;
hence SDDec2 (x,k) = SDDec y by RADIX_1:def 7; :: thesis: verum