reconsider i = i, k = k as Element of NAT by ORDINAL1:def 13;
set T = (Radix k) |^ i;
set S = (Radix k) |^ (i -' 1);
A1: Radix k <> 0 by POWER:39;
then A2: Radix k >= 1 by NAT_1:14;
A3: (Radix k) |^ i > 0 by A1, NAT_1:14, PREPOWER:19;
A4: (Radix k) |^ (i -' 1) > 0 by A1, NAT_1:14, PREPOWER:19;
then A5: 0 div ((Radix k) |^ (i -' 1)) = 0 by NAT_D:27;
defpred S₁[ Nat] means ($1 mod ((Radix k) |^ i)) div ((Radix k) |^ (i -' 1)) is Element of k -SD ;
0 in k -SD by Th16;
then A6: S₁[ 0 ] by A3, A5, NAT_D:24;
A7: for x being Nat st S₁[x] holds
S₁[x + 1]

proof

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));
reconsider R = (Radix k) - 1 as Element of NAT by A2, INT_1:16, XREAL_1:50;

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

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

(Radix k) |^ i = (Radix k) to_power i
.= 1 by A8, POWER:29 ;
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 by A4, NAT_D:27;
hence S₁[xx + 1] by Th16; :: thesis: verum

end;

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

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

end;

end;

end;

for x being Nat holds S₁[x] from NAT_1:sch 2(A6, A7);
hence (x mod ((Radix k) |^ i)) div ((Radix k) |^ (i -' 1)) is Element of k -SD ; :: thesis: verum