let m, k 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 by Def12;
1 in Seg 1 by FINSEQ_1:3;
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:234
.= (m mod ((Radix k) |^ 1)) div 1 by NEWTON:9
.= m mod ((Radix k) |^ 1) by NAT_2:6
.= m by A1, NAT_D:24 ;
:: thesis: verum