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

proof

let m, k be Nat; :: thesis: ( m >= 1 & k >= 2 implies SDDec (Fmin (m + 1),m,k) = SDDec (Fmin m,m,k) )
assume A2: ( m >= 1 & k >= 2 ) ; :: thesis: SDDec (Fmin (m + 1),m,k) = SDDec (Fmin m,m,k)
A3: m + 1 > m by NAT_1:13;
m + 1 in Seg (m + 1) by FINSEQ_1:6;
then A4: DigA (Fmin (m + 1),m,k),(m + 1) = FminDigit m,k,(m + 1) by RADIX_5:def 6
.= 0 by A2, A3, RADIX_5:def 5 ;
for i being Nat st i in Seg m holds
(Fmin (m + 1),m,k) . i = (Fmin m,m,k) . i

proof

let i be Nat; :: thesis: ( i in Seg m implies (Fmin (m + 1),m,k) . i = (Fmin m,m,k) . i )
assume A5: i in Seg m ; :: thesis: (Fmin (m + 1),m,k) . i = (Fmin m,m,k) . i
then A6: i in Seg (m + 1) by FINSEQ_2:9;
then (Fmin (m + 1),m,k) . i = DigA (Fmin (m + 1),m,k),i by RADIX_1:def 3
.= FminDigit m,k,i by A6, RADIX_5:def 6
.= DigA (Fmin m,m,k),i by A5, RADIX_5:def 6 ;
hence (Fmin (m + 1),m,k) . i = (Fmin m,m,k) . i by A5, RADIX_1:def 3; :: thesis: verum

end;

then SDDec (Fmin (m + 1),m,k) = (SDDec (Fmin m,m,k)) + (((Radix k) |^ m) * (DigA (Fmin (m + 1),m,k),(m + 1))) by RADIX_2:10;
hence SDDec (Fmin (m + 1),m,k) = SDDec (Fmin m,m,k) by A4; :: thesis: verum

end;

A7: for n being Nat st n >= 1 & S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( n >= 1 & S₁[n] implies S₁[n + 1] )
assume A8: ( n >= 1 & S₁[n] ) ; :: thesis: S₁[n + 1]
let m, k be Nat; :: thesis: ( m >= 1 & k >= 2 implies SDDec (Fmin (m + (n + 1)),m,k) = SDDec (Fmin m,m,k) )
assume A9: ( m >= 1 & k >= 2 ) ; :: thesis: SDDec (Fmin (m + (n + 1)),m,k) = SDDec (Fmin m,m,k)
m + n >= m by NAT_1:11;
then A10: (m + n) + 1 > m by NAT_1:13;
(m + n) + 1 in Seg ((m + n) + 1) by FINSEQ_1:6;
then A11: DigA (Fmin ((m + n) + 1),m,k),((m + n) + 1) = FminDigit m,k,((m + n) + 1) by RADIX_5:def 6
.= 0 by A9, A10, RADIX_5:def 5 ;
for i being Nat st i in Seg (m + n) holds
(Fmin ((m + n) + 1),m,k) . i = (Fmin (m + n),m,k) . i

proof

let i be Nat; :: thesis: ( i in Seg (m + n) implies (Fmin ((m + n) + 1),m,k) . i = (Fmin (m + n),m,k) . i )
assume A12: i in Seg (m + n) ; :: thesis: (Fmin ((m + n) + 1),m,k) . i = (Fmin (m + n),m,k) . i
then A13: i in Seg ((m + n) + 1) by FINSEQ_2:9;
then (Fmin ((m + n) + 1),m,k) . i = DigA (Fmin ((m + n) + 1),m,k),i by RADIX_1:def 3
.= FminDigit m,k,i by A13, RADIX_5:def 6
.= DigA (Fmin (m + n),m,k),i by A12, RADIX_5:def 6 ;
hence (Fmin ((m + n) + 1),m,k) . i = (Fmin (m + n),m,k) . i by A12, RADIX_1:def 3; :: thesis: verum

end;

then SDDec (Fmin (m + (n + 1)),m,k) = (SDDec (Fmin (m + n),m,k)) + (((Radix k) |^ (m + n)) * (DigA (Fmin ((m + n) + 1),m,k),((m + n) + 1))) by RADIX_2:10
.= SDDec (Fmin m,m,k) by A8, A9, A11 ;
hence SDDec (Fmin (m + (n + 1)),m,k) = SDDec (Fmin m,m,k) ; :: thesis: verum

end;

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