let n be Nat; :: thesis: ( n >= 1 implies for m, k being Nat st 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 k >= 2 holds
(SDDec (SDMax n,m,k)) + (SDDec (SDMin n,m,k)) = SDDec (DecSD 0 ,n,k)
then A2: n in Seg n by FINSEQ_1:3;
let m, k be Nat; :: thesis: ( k >= 2 implies (SDDec (SDMax n,m,k)) + (SDDec (SDMin n,m,k)) = SDDec (DecSD 0 ,n,k) )
assume A3: k >= 2 ; :: thesis: (SDDec (SDMax n,m,k)) + (SDDec (SDMin n,m,k)) = SDDec (DecSD 0 ,n,k)
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: DigA ((SDMax n,m,k) '+' (SDMin n,m,k)),i = Add (SDMax n,m,k),(SDMin n,m,k),i,k by 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 A3, 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 A3, A5, Th16
.= 0 + (SD_Add_Carry ((DigA (SDMax n,m,k),(i -' 1)) + (DigA (SDMin n,m,k),(i -' 1)))) by RADIX_1:22 ;
A7: DigA (DecSD 0 ,n,k),i = 0 by A5, Th5;
A8: i >= 1 by A5, FINSEQ_1:3;

now

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

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

then DigA (SDMin n,m,k),(i -' 1) = 0 by NAT_2:10, RADIX_1:def 3;
then DigA ((SDMax n,m,k) '+' (SDMin n,m,k)),i = SD_Add_Carry (0 + 0 ) by A6, A9, NAT_2:10, RADIX_1:def 3;
hence DigA (DecSD 0 ,n,k),i = DigA ((SDMax n,m,k) '+' (SDMin n,m,k)),i by A7, 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 A3, A6, Th16;
hence DigA (DecSD 0 ,n,k),i = DigA ((SDMax n,m,k) '+' (SDMin n,m,k)),i by A7, 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, A3, RADIX_2:11
.= (SDDec ((SDMax n,m,k) '+' (SDMin n,m,k))) + ((SD_Add_Carry 0 ) * ((Radix k) |^ n)) by A3, A2, 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