defpred S₁[ Nat] means for k being Nat st k >= 2 holds
SDDec (Fmin $1,$1,k) > 0 ;
A1: for m being Nat st m >= 1 & S₁[m] holds
S₁[m + 1]

proof

let m be Nat; :: thesis: ( m >= 1 & S₁[m] implies S₁[m + 1] )
assume that
A2: m >= 1 and
S₁[m] ; :: thesis: S₁[m + 1]
let k be Nat; :: thesis: ( k >= 2 implies SDDec (Fmin (m + 1),(m + 1),k) > 0 )
assume A3: k >= 2 ; :: thesis: SDDec (Fmin (m + 1),(m + 1),k) > 0
then Radix k > 2 by RADIX_4:1;
then A4: Radix k > 1 by XXREAL_0:2;
m + 1 in Seg (m + 1) by FINSEQ_1:6;
then A5: DigA (Fmin (m + 1),(m + 1),k),(m + 1) = FminDigit (m + 1),k,(m + 1) by RADIX_5:def 6
.= 1 by A3, RADIX_5:def 5 ;
for i being Nat st i in Seg m holds
(Fmin (m + 1),(m + 1),k) . i = (DecSD 0 ,m,k) . i

proof

let i be Nat; :: thesis: ( i in Seg m implies (Fmin (m + 1),(m + 1),k) . i = (DecSD 0 ,m,k) . i )
assume A6: i in Seg m ; :: thesis: (Fmin (m + 1),(m + 1),k) . i = (DecSD 0 ,m,k) . i
then i <= m by FINSEQ_1:3;
then A7: i < m + 1 by NAT_1:13;
A8: i in Seg (m + 1) by A6, FINSEQ_2:9;
then (Fmin (m + 1),(m + 1),k) . i = DigA (Fmin (m + 1),(m + 1),k),i by RADIX_1:def 3
.= FminDigit (m + 1),k,i by A8, RADIX_5:def 6
.= 0 by A3, A7, RADIX_5:def 5
.= DigA (DecSD 0 ,m,k),i by A6, RADIX_5:5 ;
hence (Fmin (m + 1),(m + 1),k) . i = (DecSD 0 ,m,k) . i by A6, RADIX_1:def 3; :: thesis: verum

end;

then SDDec (Fmin (m + 1),(m + 1),k) = (SDDec (DecSD 0 ,m,k)) + (((Radix k) |^ m) * (DigA (Fmin (m + 1),(m + 1),k),(m + 1))) by RADIX_2:10
.= 0 + ((Radix k) |^ m) by A2, A5, RADIX_5:6 ;
hence SDDec (Fmin (m + 1),(m + 1),k) > 0 by A4, PREPOWER:19; :: thesis: verum

end;

A9: S₁[1]

proof

let k be Nat; :: thesis: ( k >= 2 implies SDDec (Fmin 1,1,k) > 0 )
assume A10: k >= 2 ; :: thesis: SDDec (Fmin 1,1,k) > 0
A11: 1 in Seg 1 by FINSEQ_1:3;
then (DigitSD (Fmin 1,1,k)) /. 1 = SubDigit (Fmin 1,1,k),1,k by RADIX_1:def 6
.= ((Radix k) |^ (1 -' 1)) * (DigB (Fmin 1,1,k),1) by RADIX_1:def 5
.= ((Radix k) |^ (1 -' 1)) * (DigA (Fmin 1,1,k),1) by RADIX_1:def 4
.= ((Radix k) |^ 0 ) * (DigA (Fmin 1,1,k),1) by XREAL_1:234
.= 1 * (DigA (Fmin 1,1,k),1) by NEWTON:9
.= FminDigit 1,k,1 by A11, RADIX_5:def 6
.= 1 by A10, RADIX_5:def 5 ;
then A12: DigitSD (Fmin 1,1,k) = <*1*> by RADIX_1:20;
SDDec (Fmin 1,1,k) = Sum (DigitSD (Fmin 1,1,k)) by RADIX_1:def 7
.= 1 by A12, RVSUM_1:103 ;
hence SDDec (Fmin 1,1,k) > 0 ; :: thesis: verum

end;

for m being Nat st m >= 1 holds
S₁[m] from NAT_1:sch 8(A9, A1);
hence for m, k being Nat st m >= 1 & k >= 2 holds
SDDec (Fmin m,m,k) > 0 ; :: thesis: verum