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, Th15;
then SD_Add_Data (((DigA (x,i)) + (DigA (y,i))),k) <= (Radix k) - 2 by A2, Th19;
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:7;
(- (Radix k)) + 2 <= SD_Add_Data (((DigA (x,i)) + (DigA (y,i))),k) by A2, A5, Th19;
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:7;
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