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 S1[ 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;
then A3: (Radix k) |^ (i -' 1) > 0 by NAT_1:14, PREPOWER:11;
then A4: 0 div ((Radix k) |^ (i -' 1)) = 0 by NAT_D:27;
A5: Radix k >= 1 by A2, NAT_1:14;
A6: for x being Nat st S1[x] holds
S1[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: ( S1[xx] implies S1[xx + 1] )
assume (xx mod ((Radix k) |^ i)) div ((Radix k) |^ (i -' 1)) is Element of k -SD ; :: thesis: S1[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: S1[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 by A3, NAT_D:27;
hence S1[xx + 1] by Th13; :: thesis: verum
end;
suppose A8: i > 0 ; :: thesis: S1[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 S1[xx + 1] ; :: thesis: verum
end;
end;
end;
(Radix k) |^ i > 0 by A2, NAT_1:14, PREPOWER:11;
then A10: S1[ 0 ] by A4, A1, NAT_D:24;
for x being Nat holds S1[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