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:3;

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:5

.= 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

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:3;

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:5

.= 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