reconsider i = i, k = k as Element of NAT by ORDINAL1:def 12;
set T = (Radix k) |^ i;
set S = (Radix k) |^ (i -' 1);
defpred S₁[ Nat] means ($1 mod ((Radix k) |^ i)) div ((Radix k) |^ (i -' 1)) is Element of k -SD ;
A1: 0 in k -SD by Th13;
A2: Radix k <> 0 by POWER:34;
A4: 0 div ((Radix k) |^ (i -' 1)) = 0 ;
A5: Radix k >= 1 by A2, NAT_1:14;
A6: for x being Nat st S₁[x] holds
S₁[x + 1]

proof

reconsider R = (Radix k) - 1 as Element of NAT by A5, INT_1:3, XREAL_1:48;
let xx be Nat; :: thesis: ( S₁[xx] implies S₁[xx + 1] )
assume (xx mod ((Radix k) |^ i)) div ((Radix k) |^ (i -' 1)) is Element of k -SD ; :: thesis: S₁[xx + 1]
set X = ((xx + 1) mod ((Radix k) |^ i)) div ((Radix k) |^ (i -' 1));

per cases ( i = 0 or i > 0 ) ;

suppose A7: i = 0 ; :: thesis: S₁[xx + 1]

(Radix k) |^ i = (Radix k) to_power i
.= 1 by A7, POWER:24 ;
then (xx + 1) mod ((Radix k) |^ i) = ((xx + 1) * 1) mod 1
.= 0 by NAT_D:13 ;
then ((xx + 1) mod ((Radix k) |^ i)) div ((Radix k) |^ (i -' 1)) = 0 ;
hence S₁[xx + 1] by Th13; :: thesis: verum

end;

suppose A8: i > 0 ; :: thesis: S₁[xx + 1]

- 1 >= - (Radix k) by A5, XREAL_1:24;
then A9: ( ((xx + 1) mod ((Radix k) |^ i)) div ((Radix k) |^ (i -' 1)) is Element of INT & 0 >= (- (Radix k)) + 1 ) by INT_1:def 2, XREAL_1:59;
((xx + 1) mod ((Radix k) |^ i)) div ((Radix k) |^ (i -' 1)) < ((Radix k) - 1) + 1 by A2, A8, Th5;
then ((xx + 1) mod ((Radix k) |^ i)) div ((Radix k) |^ (i -' 1)) <= R by NAT_1:13;
then ((xx + 1) mod ((Radix k) |^ i)) div ((Radix k) |^ (i -' 1)) in k -SD by A9;
hence S₁[xx + 1] ; :: thesis: verum

end;

end;

end;

(Radix k) |^ i > 0 by A2, NAT_1:14, PREPOWER:11;
then A10: S₁[ 0 ] by A4, A1, NAT_D:24;
for x being Nat holds S₁[x] from NAT_1:sch 2(A10, A6);
hence (x mod ((Radix k) |^ i)) div ((Radix k) |^ (i -' 1)) is Element of k -SD ; :: thesis: verum