set SDC = SD_Add_Carry ((DigA x,(i -' 1)) + (DigA y,(i -' 1)));
set SDD = SD_Add_Data ((DigA x,i) + (DigA y,i)),k;
A3: - 1 <= SD_Add_Carry ((DigA x,(i -' 1)) + (DigA y,(i -' 1))) by Lm2;
A4: SD_Add_Carry ((DigA x,(i -' 1)) + (DigA y,(i -' 1))) <= 1 by Lm2;
A5: ( DigA x,i is Element of k -SD & DigA y,i is Element of k -SD ) by A1, Th19;
then SD_Add_Data ((DigA x,i) + (DigA y,i)),k <= (Radix k) - 2 by A2, Th23;
then A6: (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 A4, XREAL_1:9;
(- (Radix k)) + 2 <= SD_Add_Data ((DigA x,i) + (DigA y,i)),k by A2, A5, Th23;
then ( (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 & ((- (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)))) ) by A3, INT_1:def 2, 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 A6;
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