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: 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 that
n >= 1 and
A2: 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 that
A3: m >= 1 and
A4: k >= 2 ; :: thesis: SDDec (Fmin (m + (n + 1)),m,k) = SDDec (Fmin m,m,k)
m + n >= m by NAT_1:11;
then A5: (m + n) + 1 > m by NAT_1:13;
(m + n) + 1 in Seg ((m + n) + 1) by FINSEQ_1:6;
then A6: DigA (Fmin ((m + n) + 1),m,k),((m + n) + 1) = FminDigit m,k,((m + n) + 1) by RADIX_5:def 6
.= 0 by A4, A5, 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 A7: i in Seg (m + n) ; :: thesis: (Fmin ((m + n) + 1),m,k) . i = (Fmin (m + n),m,k) . i
then A8: 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 A8, RADIX_5:def 6
.= DigA (Fmin (m + n),m,k),i by A7, RADIX_5:def 6 ;
hence (Fmin ((m + n) + 1),m,k) . i = (Fmin (m + n),m,k) . i by A7, 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 A2, A3, A4, A6 ;
hence SDDec (Fmin (m + (n + 1)),m,k) = SDDec (Fmin m,m,k) ; :: thesis: verum

end;

A9: 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 that
m >= 1 and
A10: k >= 2 ; :: thesis: SDDec (Fmin (m + 1),m,k) = SDDec (Fmin m,m,k)
A11: m + 1 > m by NAT_1:13;
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 A12: i in Seg m ; :: thesis: (Fmin (m + 1),m,k) . i = (Fmin m,m,k) . i
then A13: 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 A13, RADIX_5:def 6
.= DigA (Fmin m,m,k),i by A12, RADIX_5:def 6 ;
hence (Fmin (m + 1),m,k) . i = (Fmin m,m,k) . i by A12, RADIX_1:def 3; :: thesis: verum

end;

then A14: 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;
m + 1 in Seg (m + 1) by FINSEQ_1:6;
then DigA (Fmin (m + 1),m,k),(m + 1) = FminDigit m,k,(m + 1) by RADIX_5:def 6
.= 0 by A10, A11, RADIX_5:def 5 ;
hence SDDec (Fmin (m + 1),m,k) = SDDec (Fmin m,m,k) by A14; :: thesis: verum

end;

for n being Nat st n >= 1 holds
S₁[n] from NAT_1:sch 8(A9, A1);
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