let f, m, k be Nat; :: thesis: ( m >= 1 & k >= 2 & f needs_digits_of m,k implies f >= SDDec (Fmin (m + 2),m,k) )
assume that
A1: m >= 1 and
A2: k >= 2 and
A3: f needs_digits_of m,k ; :: thesis: f >= SDDec (Fmin (m + 2),m,k)
for i being Nat st i in Seg m holds
DigA (DecSD f,m,k),i >= DigA (Fmin m,m,k),i

proof

let i be Nat; :: thesis: ( i in Seg m implies DigA (DecSD f,m,k),i >= DigA (Fmin m,m,k),i )
assume A4: i in Seg m ; :: thesis: DigA (DecSD f,m,k),i >= DigA (Fmin m,m,k),i
then A5: i <= m by FINSEQ_1:3;

now

per cases ( i = m or i < m ) by A5, XXREAL_0:1;

suppose A6: i = m ; :: thesis: DigA (DecSD f,m,k),i >= DigA (Fmin m,m,k),i

then DigA (DecSD f,m,k),i > 0 by A1, A3, Th6;
then A7: DigA (DecSD f,m,k),i >= 0 + 1 by INT_1:20;
DigA (Fmin m,m,k),i = FminDigit m,k,i by A4, RADIX_5:def 6
.= 1 by A2, A6, RADIX_5:def 5 ;
hence DigA (DecSD f,m,k),i >= DigA (Fmin m,m,k),i by A7; :: thesis: verum

end;

suppose A8: i < m ; :: thesis: DigA (DecSD f,m,k),i >= DigA (Fmin m,m,k),i

DigA (Fmin m,m,k),i = FminDigit m,k,i by A4, RADIX_5:def 6
.= 0 by A2, A8, RADIX_5:def 5 ;
hence DigA (DecSD f,m,k),i >= DigA (Fmin m,m,k),i by A4, Th5; :: thesis: verum

end;

end;

end;

hence DigA (DecSD f,m,k),i >= DigA (Fmin m,m,k),i ; :: thesis: verum

end;

then SDDec (DecSD f,m,k) >= SDDec (Fmin m,m,k) by A1, RADIX_5:13;
then A9: SDDec (DecSD f,m,k) >= SDDec (Fmin (m + 2),m,k) by A1, A2, Th1;
f < (Radix k) |^ m by A3, Def7;
then f is_represented_by m,k by RADIX_1:def 12;
hence f >= SDDec (Fmin (m + 2),m,k) by A1, A9, RADIX_1:25; :: thesis: verum