let n, m, k be Nat; :: thesis: ( m in Seg n & k >= 2 implies SDDec (Fmin (n + 1),(m + 1),k) = (SDDec (Fmin (n + 1),m,k)) + (SDDec (Fmax (n + 1),m,k)) )
assume A1: ( m in Seg n & k >= 2 ) ; :: thesis: SDDec (Fmin (n + 1),(m + 1),k) = (SDDec (Fmin (n + 1),m,k)) + (SDDec (Fmax (n + 1),m,k))
then A2: ( n >= m & m >= 1 ) by FINSEQ_1:3;
then A3: n + 1 > m by NAT_1:13;
A4: n + 1 >= 1 by NAT_1:11;
A5: n + 1 in Seg (n + 1) by FINSEQ_1:5;
then A6: DigA (Fmin (n + 1),m,k),(n + 1) = FminDigit m,k,(n + 1) by Def6
.= 0 by A1, A3, Def5 ;
A7: DigA (Fmax (n + 1),m,k),(n + 1) = FmaxDigit m,k,(n + 1) by A5, Def8
.= 0 by A1, A3, Def7 ;
A8: (SDDec (Fmin (n + 1),m,k)) + (SDDec (Fmax (n + 1),m,k)) = (SDDec ((Fmin (n + 1),m,k) '+' (Fmax (n + 1),m,k))) + ((SD_Add_Carry ((DigA (Fmin (n + 1),m,k),(n + 1)) + (DigA (Fmax (n + 1),m,k),(n + 1)))) * ((Radix k) |^ (n + 1))) by A1, NAT_1:11, RADIX_2:11
.= (SDDec ((Fmin (n + 1),m,k) '+' (Fmax (n + 1),m,k))) + (0 * ((Radix k) |^ (n + 1))) by A6, A7, RADIX_1:21 ;
A9: m in Seg (n + 1) by A1, FINSEQ_2:9;
for i being Nat st i in Seg (n + 1) holds
DigA (Fmin (n + 1),(m + 1),k),i = DigA ((Fmin (n + 1),m,k) '+' (Fmax (n + 1),m,k)),i

proof

let i be Nat; :: thesis: ( i in Seg (n + 1) implies DigA (Fmin (n + 1),(m + 1),k),i = DigA ((Fmin (n + 1),m,k) '+' (Fmax (n + 1),m,k)),i )
assume A10: i in Seg (n + 1) ; :: thesis: DigA (Fmin (n + 1),(m + 1),k),i = DigA ((Fmin (n + 1),m,k) '+' (Fmax (n + 1),m,k)),i
then A11: DigA ((Fmin (n + 1),m,k) '+' (Fmax (n + 1),m,k)),i = Add (Fmin (n + 1),m,k),(Fmax (n + 1),m,k),i,k by RADIX_1:def 14
.= (SD_Add_Data ((DigA (Fmin (n + 1),m,k),i) + (DigA (Fmax (n + 1),m,k),i)),k) + (SD_Add_Carry ((DigA (Fmin (n + 1),m,k),(i -' 1)) + (DigA (Fmax (n + 1),m,k),(i -' 1)))) by A1, A10, RADIX_1:def 13 ;
A12: m + 1 > m by NAT_1:13;
A13: DigA (Fmin (n + 1),m,k),i = FminDigit m,k,i by A10, Def6;
A14: DigA (Fmax (n + 1),m,k),i = FmaxDigit m,k,i by A10, Def8;
A15: DigA (Fmin (n + 1),(m + 1),k),i = FminDigit (m + 1),k,i by A10, Def6;
A16: i >= 1 by A10, FINSEQ_1:3;

now

per cases ( i >= m + 1 or i < m + 1 ) ;

suppose A17: i >= m + 1 ; :: thesis: DigA (Fmin (n + 1),(m + 1),k),i = DigA ((Fmin (n + 1),m,k) '+' (Fmax (n + 1),m,k)),i

now

per cases ( i = m + 1 or i <> m + 1 ) ;

suppose A18: i = m + 1 ; :: thesis: DigA (Fmin (n + 1),(m + 1),k),i = DigA ((Fmin (n + 1),m,k) '+' (Fmax (n + 1),m,k)),i

then A19: DigA (Fmin (n + 1),m,k),i = FminDigit m,k,(m + 1) by A10, Def6
.= 0 by A1, A12, Def5 ;
A20: DigA (Fmax (n + 1),m,k),i = FmaxDigit m,k,(m + 1) by A10, A18, Def8
.= 0 by A1, A12, Def7 ;
A21: DigA (Fmin (n + 1),m,k),(i -' 1) = DigA (Fmin (n + 1),m,k),m by A18, NAT_D:34
.= FminDigit m,k,m by A9, Def6
.= 1 by A1, Def5 ;
A22: DigA (Fmax (n + 1),m,k),(i -' 1) = DigA (Fmax (n + 1),m,k),m by A18, NAT_D:34
.= FmaxDigit m,k,m by A9, Def8
.= (Radix k) - 1 by A1, Def7 ;
A23: DigA (Fmin (n + 1),(m + 1),k),i = FminDigit (m + 1),k,(m + 1) by A10, A18, Def6
.= 1 by A1, Def5 ;
DigA ((Fmin (n + 1),m,k) '+' (Fmax (n + 1),m,k)),i = 0 + (SD_Add_Carry (1 + ((Radix k) - 1))) by A11, A19, A20, A21, A22, RADIX_1:22
.= 1 by A1, Th10 ;
hence DigA (Fmin (n + 1),(m + 1),k),i = DigA ((Fmin (n + 1),m,k) '+' (Fmax (n + 1),m,k)),i by A23; :: thesis: verum

end;

suppose A24: i <> m + 1 ; :: thesis: DigA (Fmin (n + 1),(m + 1),k),i = DigA ((Fmin (n + 1),m,k) '+' (Fmax (n + 1),m,k)),i

then A25: i > m + 1 by A17, XXREAL_0:1;
i > m by A17, NAT_1:13;
then i > 1 by A2, XXREAL_0:2;
then A26: i -' 1 in Seg (n + 1) by A10, Th2;
i - 1 > (m + 1) - 1 by A25, XREAL_1:16;
then A27: i -' 1 > m by XREAL_0:def 2;
A28: DigA (Fmin (n + 1),m,k),i = 0 by A1, A12, A13, A17, Def5;
A29: DigA (Fmax (n + 1),m,k),i = 0 by A1, A12, A14, A17, Def7;
A30: DigA (Fmin (n + 1),m,k),(i -' 1) = FminDigit m,k,(i -' 1) by A26, Def6
.= 0 by A1, A27, Def5 ;
A31: DigA (Fmax (n + 1),m,k),(i -' 1) = FmaxDigit m,k,(i -' 1) by A26, Def8
.= 0 by A1, A27, Def7 ;
DigA (Fmin (n + 1),(m + 1),k),i = 0 by A1, A15, A24, Def5;
hence DigA (Fmin (n + 1),(m + 1),k),i = DigA ((Fmin (n + 1),m,k) '+' (Fmax (n + 1),m,k)),i by A11, A28, A29, A30, A31, RADIX_1:21, RADIX_1:22; :: thesis: verum

end;

end;

end;

hence DigA (Fmin (n + 1),(m + 1),k),i = DigA ((Fmin (n + 1),m,k) '+' (Fmax (n + 1),m,k)),i ; :: thesis: verum

end;

suppose i < m + 1 ; :: thesis: DigA (Fmin (n + 1),(m + 1),k),i = DigA ((Fmin (n + 1),m,k) '+' (Fmax (n + 1),m,k)),i

then A32: i <= m by NAT_1:13;

now

per cases ( i > 1 or i = 1 ) by A16, XXREAL_0:1;

suppose A33: i > 1 ; :: thesis: DigA (Fmin (n + 1),(m + 1),k),i = DigA ((Fmin (n + 1),m,k) '+' (Fmax (n + 1),m,k)),i

then A34: m > 1 by A32, XXREAL_0:2;
then A35: m -' 1 in Seg (n + 1) by A9, Th2;
A36: m -' 1 < m by A34, JORDAN5B:1;

now

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

suppose A37: i = m ; :: thesis: DigA (Fmin (n + 1),(m + 1),k),i = DigA ((Fmin (n + 1),m,k) '+' (Fmax (n + 1),m,k)),i

then A38: DigA (Fmax (n + 1),m,k),i = (Radix k) - 1 by A1, A14, Def7;
A39: DigA (Fmin (n + 1),m,k),(i -' 1) = FminDigit m,k,(m -' 1) by A35, A37, Def6
.= 0 by A1, A36, Def5 ;
A40: DigA (Fmax (n + 1),m,k),(i -' 1) = FmaxDigit m,k,(m -' 1) by A35, A37, Def8
.= 0 by A1, A36, Def7 ;
A41: DigA (Fmin (n + 1),(m + 1),k),i = FminDigit (m + 1),k,m by A10, A37, Def6
.= 0 by A1, A12, Def5 ;
DigA ((Fmin (n + 1),m,k) '+' (Fmax (n + 1),m,k)),i = (SD_Add_Data (1 + ((Radix k) - 1)),k) + 0 by A1, A11, A13, A37, A38, A39, A40, Def5, RADIX_1:21
.= 0 by A1, Th11 ;
hence DigA (Fmin (n + 1),(m + 1),k),i = DigA ((Fmin (n + 1),m,k) '+' (Fmax (n + 1),m,k)),i by A41; :: thesis: verum

end;

suppose A42: i < m ; :: thesis: DigA (Fmin (n + 1),(m + 1),k),i = DigA ((Fmin (n + 1),m,k) '+' (Fmax (n + 1),m,k)),i

A43: i -' 1 < i by A16, JORDAN5B:1;
then i -' 1 < m by A42, XXREAL_0:2;
then A44: i -' 1 <= n + 1 by A3, XXREAL_0:2;
i -' 1 >= 1 by A33, NAT_D:49;
then A45: i -' 1 in Seg (n + 1) by A44, FINSEQ_1:3;
A46: DigA (Fmax (n + 1),m,k),i = 0 by A1, A14, A42, Def7;
A47: DigA (Fmin (n + 1),m,k),(i -' 1) = FminDigit m,k,(i -' 1) by A45, Def6
.= 0 by A1, A42, A43, Def5 ;
A48: DigA (Fmax (n + 1),m,k),(i -' 1) = FmaxDigit m,k,(i -' 1) by A45, Def8
.= 0 by A1, A42, A43, Def7 ;
A49: i < m + 1 by A42, NAT_1:13;
DigA ((Fmin (n + 1),m,k) '+' (Fmax (n + 1),m,k)),i = (SD_Add_Data (0 + 0 ),k) + (SD_Add_Carry (0 + 0 )) by A1, A11, A13, A42, A46, A47, A48, Def5
.= 0 + 0 by RADIX_1:21, RADIX_1:22 ;
hence DigA (Fmin (n + 1),(m + 1),k),i = DigA ((Fmin (n + 1),m,k) '+' (Fmax (n + 1),m,k)),i by A1, A15, A49, Def5; :: thesis: verum

end;

end;

end;

hence DigA (Fmin (n + 1),(m + 1),k),i = DigA ((Fmin (n + 1),m,k) '+' (Fmax (n + 1),m,k)),i ; :: thesis: verum

end;

suppose i = 1 ; :: thesis: DigA (Fmin (n + 1),(m + 1),k),i = DigA ((Fmin (n + 1),m,k) '+' (Fmax (n + 1),m,k)),i

then A50: i -' 1 = 0 by NAT_2:10;
then A51: DigA (Fmax (n + 1),m,k),(i -' 1) = 0 by RADIX_1:def 3;

now

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

suppose A52: i < m ; :: thesis: DigA (Fmin (n + 1),(m + 1),k),i = DigA ((Fmin (n + 1),m,k) '+' (Fmax (n + 1),m,k)),i

then A53: DigA (Fmin (n + 1),m,k),i = 0 by A1, A13, Def5;
A54: DigA (Fmax (n + 1),m,k),i = 0 by A1, A14, A52, Def7;
A55: i < m + 1 by A52, NAT_1:13;
DigA ((Fmin (n + 1),m,k) '+' (Fmax (n + 1),m,k)),i = (SD_Add_Data (0 + 0 ),k) + (SD_Add_Carry (0 + 0 )) by A11, A50, A51, A53, A54, RADIX_1:def 3
.= 0 + 0 by RADIX_1:21, RADIX_1:22 ;
hence DigA (Fmin (n + 1),(m + 1),k),i = DigA ((Fmin (n + 1),m,k) '+' (Fmax (n + 1),m,k)),i by A1, A15, A55, Def5; :: thesis: verum

end;

suppose A56: i = m ; :: thesis: DigA (Fmin (n + 1),(m + 1),k),i = DigA ((Fmin (n + 1),m,k) '+' (Fmax (n + 1),m,k)),i

then A57: DigA (Fmin (n + 1),m,k),i = 1 by A1, A13, Def5;
A58: DigA (Fmax (n + 1),m,k),i = (Radix k) - 1 by A1, A14, A56, Def7;
A59: i < m + 1 by A56, NAT_1:13;
DigA ((Fmin (n + 1),m,k) '+' (Fmax (n + 1),m,k)),i = (SD_Add_Data (1 + ((Radix k) - 1)),k) + 0 by A11, A50, A51, A57, A58, RADIX_1:21, RADIX_1:def 3
.= 0 by A1, Th11 ;
hence DigA (Fmin (n + 1),(m + 1),k),i = DigA ((Fmin (n + 1),m,k) '+' (Fmax (n + 1),m,k)),i by A1, A15, A59, Def5; :: thesis: verum

end;

end;

end;

hence DigA (Fmin (n + 1),(m + 1),k),i = DigA ((Fmin (n + 1),m,k) '+' (Fmax (n + 1),m,k)),i ; :: thesis: verum

end;

end;

end;

hence DigA (Fmin (n + 1),(m + 1),k),i = DigA ((Fmin (n + 1),m,k) '+' (Fmax (n + 1),m,k)),i ; :: thesis: verum

end;

end;

end;

hence DigA (Fmin (n + 1),(m + 1),k),i = DigA ((Fmin (n + 1),m,k) '+' (Fmax (n + 1),m,k)),i ; :: thesis: verum

end;

hence SDDec (Fmin (n + 1),(m + 1),k) = (SDDec (Fmin (n + 1),m,k)) + (SDDec (Fmax (n + 1),m,k)) by A4, A8, Th12; :: thesis: verum