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:4, TARSKI:def 1;
then A3: (DigitSD x) /. 1 = SubDigit x,1,k by RADIX_1:def 6;
A4: len (DigitSD x) = 1 by FINSEQ_1:def 18;
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 8;
thus SDDec x = Sum (DigitSD x) by RADIX_1:def 7
.= Sum <*(SubDigit x,1,k)*> by A4, A5, FINSEQ_1:57
.= SubDigit x,1,k by RVSUM_1:103
.= ((Radix k) |^ 0 ) * (DigB x,1) by A1, RADIX_1:def 5
.= 1 * (DigB x,1) by NEWTON:9
.= DigA x,1 by RADIX_1:def 4 ; :: thesis: verum