let n be Nat; :: thesis: ( n >= 1 implies for m, k being Nat st m in Seg n & k >= 2 holds
(SDDec (SDMax n,m,k)) + (SDDec (SDMin n,m,k)) = SDDec (DecSD 0 ,n,k) )
assume A1: n >= 1 ; :: thesis: for m, k being Nat st m in Seg n & k >= 2 holds
(SDDec (SDMax n,m,k)) + (SDDec (SDMin n,m,k)) = SDDec (DecSD 0 ,n,k)
let m, k be Nat; :: thesis: ( m in Seg n & k >= 2 implies (SDDec (SDMax n,m,k)) + (SDDec (SDMin n,m,k)) = SDDec (DecSD 0 ,n,k) )
assume A2: ( m in Seg n & k >= 2 ) ; :: thesis: (SDDec (SDMax n,m,k)) + (SDDec (SDMin n,m,k)) = SDDec (DecSD 0 ,n,k)
A3: n in Seg n by A1, FINSEQ_1:3;
A4: for i being Nat st i in Seg n holds
DigA (DecSD 0 ,n,k),i = DigA ((SDMax n,m,k) '+' (SDMin n,m,k)),i

proof

let i be Nat; :: thesis: ( i in Seg n implies DigA (DecSD 0 ,n,k),i = DigA ((SDMax n,m,k) '+' (SDMin n,m,k)),i )
assume A5: i in Seg n ; :: thesis: DigA (DecSD 0 ,n,k),i = DigA ((SDMax n,m,k) '+' (SDMin n,m,k)),i
then A6: ( i >= 1 & i <= n ) by FINSEQ_1:3;
A7: DigA ((SDMax n,m,k) '+' (SDMin n,m,k)),i = Add (SDMax n,m,k),(SDMin n,m,k),i,k by A5, RADIX_1:def 14
.= (SD_Add_Data ((DigA (SDMax n,m,k),i) + (DigA (SDMin n,m,k),i)),k) + (SD_Add_Carry ((DigA (SDMax n,m,k),(i -' 1)) + (DigA (SDMin n,m,k),(i -' 1)))) by A2, A5, RADIX_1:def 13
.= (SD_Add_Data 0 ,k) + (SD_Add_Carry ((DigA (SDMax n,m,k),(i -' 1)) + (DigA (SDMin n,m,k),(i -' 1)))) by A1, A2, A5, Th16
.= 0 + (SD_Add_Carry ((DigA (SDMax n,m,k),(i -' 1)) + (DigA (SDMin n,m,k),(i -' 1)))) by RADIX_1:22 ;
A8: DigA (DecSD 0 ,n,k),i = 0 by A5, Th5;

now

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

suppose i = 1 ; :: thesis: DigA (DecSD 0 ,n,k),i = DigA ((SDMax n,m,k) '+' (SDMin n,m,k)),i

then A9: i -' 1 = 0 by NAT_2:10;
then DigA (SDMin n,m,k),(i -' 1) = 0 by RADIX_1:def 3;
then DigA ((SDMax n,m,k) '+' (SDMin n,m,k)),i = SD_Add_Carry (0 + 0 ) by A7, A9, RADIX_1:def 3;
hence DigA (DecSD 0 ,n,k),i = DigA ((SDMax n,m,k) '+' (SDMin n,m,k)),i by A8, RADIX_1:def 10; :: thesis: verum

end;

suppose i > 1 ; :: thesis: DigA (DecSD 0 ,n,k),i = DigA ((SDMax n,m,k) '+' (SDMin n,m,k)),i

then i -' 1 in Seg n by A5, Th2;
then DigA ((SDMax n,m,k) '+' (SDMin n,m,k)),i = SD_Add_Carry 0 by A1, A2, A7, Th16;
hence DigA (DecSD 0 ,n,k),i = DigA ((SDMax n,m,k) '+' (SDMin n,m,k)),i by A8, RADIX_1:def 10; :: thesis: verum

end;

end;

end;

hence DigA (DecSD 0 ,n,k),i = DigA ((SDMax n,m,k) '+' (SDMin n,m,k)),i ; :: thesis: verum

end;

(SDDec (SDMax n,m,k)) + (SDDec (SDMin n,m,k)) = (SDDec ((SDMax n,m,k) '+' (SDMin n,m,k))) + ((SD_Add_Carry ((DigA (SDMax n,m,k),n) + (DigA (SDMin n,m,k),n))) * ((Radix k) |^ n)) by A1, A2, RADIX_2:11
.= (SDDec ((SDMax n,m,k) '+' (SDMin n,m,k))) + ((SD_Add_Carry 0 ) * ((Radix k) |^ n)) by A1, A2, A3, Th16
.= (SDDec ((SDMax n,m,k) '+' (SDMin n,m,k))) + (0 * ((Radix k) |^ n)) by RADIX_1:def 10 ;
hence (SDDec (SDMax n,m,k)) + (SDDec (SDMin n,m,k)) = SDDec (DecSD 0 ,n,k) by A1, A4, Th12; :: thesis: verum