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:4;
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:8;
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:8;
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:4;
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