let m, n, k be Nat; :: thesis: ( m is_represented_by n + 1,k implies DigA (DecSD m,(n + 1),k),(n + 1) = m div ((Radix k) |^ n) )
assume A1: m is_represented_by n + 1,k ; :: thesis: DigA (DecSD m,(n + 1),k),(n + 1) = m div ((Radix k) |^ n)
A2: n + 1 in Seg (n + 1) by FINSEQ_1:5;
A3: m < (Radix k) |^ (n + 1) by A1, Def12;
DigA (DecSD m,(n + 1),k),(n + 1) = DigitDC m,(n + 1),k by A2, Def9
.= m div ((Radix k) |^ ((n + 1) -' 1)) by A3, NAT_D:24
.= m div ((Radix k) |^ n) by NAT_D:34 ;
hence DigA (DecSD m,(n + 1),k),(n + 1) = m div ((Radix k) |^ n) ; :: thesis: verum