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

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