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