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:4;
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:1;
then A7: i < m + 1 by NAT_1:13;
A8: i in Seg (m + 1) by A6, FINSEQ_2:8;
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:11; :: 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:1;
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:232
.= 1 * (DigA ((Fmin (1,1,k)),1)) by NEWTON:4
.= 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:17;
SDDec (Fmin (1,1,k)) = Sum (DigitSD (Fmin (1,1,k))) by RADIX_1:def 7
.= 1 by A12, RVSUM_1:73 ;
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