let k, x, n be Nat; :: thesis: ( n >= 1 implies DigA (DecSD (x mod ((Radix k) |^ n)),n,k),n = DigA (DecSD x,n,k),n )
set xn = x mod ((Radix k) |^ n);
assume n >= 1 ; :: thesis: DigA (DecSD (x mod ((Radix k) |^ n)),n,k),n = DigA (DecSD x,n,k),n
then n <> 0 ;
then A1: n in Seg n by FINSEQ_1:5;
then DigA (DecSD (x mod ((Radix k) |^ n)),n,k),n = DigitDC (x mod ((Radix k) |^ n)),n,k by RADIX_1:def 9
.= DigitDC x,n,k by EULER_2:7
.= DigA (DecSD x,n,k),n by A1, RADIX_1:def 9 ;
hence DigA (DecSD (x mod ((Radix k) |^ n)),n,k),n = DigA (DecSD x,n,k),n ; :: thesis: verum