set SDD = SD_Add_Data ((DigA x,i) + (DigA y,i)),k;
set SDC = SD_Add_Carry ((DigA x,(i -' 1)) + (DigA y,(i -' 1)));
A2: DigA x,i is Element of k -SD by A1, Th19;
DigA y,i is Element of k -SD by A1, Th19;
then A3: ( (- (Radix k)) + 2 <= SD_Add_Data ((DigA x,i) + (DigA y,i)),k & SD_Add_Data ((DigA x,i) + (DigA y,i)),k <= (Radix k) - 2 ) by A1, A2, Th23;
A4: (SD_Add_Data ((DigA x,i) + (DigA y,i)),k) + (SD_Add_Carry ((DigA x,(i -' 1)) + (DigA y,(i -' 1)))) is Element of INT by INT_1:def 2;
( - 1 <= SD_Add_Carry ((DigA x,(i -' 1)) + (DigA y,(i -' 1))) & SD_Add_Carry ((DigA x,(i -' 1)) + (DigA y,(i -' 1))) <= 1 ) by Lm2;
then ( ((- (Radix k)) + 2) + (- 1) <= (SD_Add_Data ((DigA x,i) + (DigA y,i)),k) + (SD_Add_Carry ((DigA x,(i -' 1)) + (DigA y,(i -' 1)))) & (SD_Add_Data ((DigA x,i) + (DigA y,i)),k) + (SD_Add_Carry ((DigA x,(i -' 1)) + (DigA y,(i -' 1)))) <= ((Radix k) - 2) + 1 ) by A3, XREAL_1:9;
then (SD_Add_Data ((DigA x,i) + (DigA y,i)),k) + (SD_Add_Carry ((DigA x,(i -' 1)) + (DigA y,(i -' 1)))) in k -SD by A4;
hence (SD_Add_Data ((DigA x,i) + (DigA y,i)),k) + (SD_Add_Carry ((DigA x,(i -' 1)) + (DigA y,(i -' 1)))) is Element of k -SD ; :: thesis: verum