let k be Nat; :: thesis: for x being Tuple of 1,k -SD holds SDDec x = DigA (x,1)

1 - 1 = 0 ;

then A1: 1 -' 1 = 0 by XREAL_0:def 2;

let x be Tuple of 1,k -SD ; :: thesis: SDDec x = DigA (x,1)

A2: 1 in Seg 1 by FINSEQ_1:2, TARSKI:def 1;

then A3: (DigitSD x) /. 1 = SubDigit (x,1,k) by RADIX_1:def 6;

A4: len (DigitSD x) = 1 by CARD_1:def 7;

then 1 in dom (DigitSD x) by A2, FINSEQ_1:def 3;

then A5: (DigitSD x) . 1 = SubDigit (x,1,k) by A3, PARTFUN1:def 6;

thus SDDec x = Sum (DigitSD x) by RADIX_1:def 7

.= Sum <*(SubDigit (x,1,k))*> by A4, A5, FINSEQ_1:40

.= SubDigit (x,1,k) by RVSUM_1:73

.= ((Radix k) |^ 0) * (DigB (x,1)) by A1, RADIX_1:def 5

.= 1 * (DigB (x,1)) by NEWTON:4

.= DigA (x,1) by RADIX_1:def 4 ; :: thesis: verum

1 - 1 = 0 ;

then A1: 1 -' 1 = 0 by XREAL_0:def 2;

let x be Tuple of 1,k -SD ; :: thesis: SDDec x = DigA (x,1)

A2: 1 in Seg 1 by FINSEQ_1:2, TARSKI:def 1;

then A3: (DigitSD x) /. 1 = SubDigit (x,1,k) by RADIX_1:def 6;

A4: len (DigitSD x) = 1 by CARD_1:def 7;

then 1 in dom (DigitSD x) by A2, FINSEQ_1:def 3;

then A5: (DigitSD x) . 1 = SubDigit (x,1,k) by A3, PARTFUN1:def 6;

thus SDDec x = Sum (DigitSD x) by RADIX_1:def 7

.= Sum <*(SubDigit (x,1,k))*> by A4, A5, FINSEQ_1:40

.= SubDigit (x,1,k) by RVSUM_1:73

.= ((Radix k) |^ 0) * (DigB (x,1)) by A1, RADIX_1:def 5

.= 1 * (DigB (x,1)) by NEWTON:4

.= DigA (x,1) by RADIX_1:def 4 ; :: thesis: verum