let n, k be Nat; :: thesis: for x being Tuple of , NAT
for y being Tuple of ,k -SD st x = y holds
SDDec2 x,k = SDDec y
let x be Tuple of , NAT ; :: thesis: for y being Tuple of ,k -SD st x = y holds
SDDec2 x,k = SDDec y
let y be Tuple of ,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