let k, m be Nat; :: thesis: ( m is_represented_by 1,k implies DigA ((DecSD (m,1,k)),1) = m )
assume m is_represented_by 1,k ; :: thesis: DigA ((DecSD (m,1,k)),1) = m
then A1: m < (Radix k) |^ 1 ;
1 in Seg 1 by FINSEQ_1:1;
hence DigA ((DecSD (m,1,k)),1) = DigitDC (m,1,k) by Def9
.= (m mod ((Radix k) |^ 1)) div ((Radix k) |^ 0) by XREAL_1:232
.= (m mod ((Radix k) |^ 1)) div 1 by NEWTON:4
.= m mod ((Radix k) |^ 1) by NAT_2:4
.= m by A1, NAT_D:24 ;
:: thesis: verum