set SDAD = SDSub_Add_Data ((DigA_SDSub x,i) + (DigA_SDSub y,i)),k;
set SDAC = SDSub_Add_Carry ((DigA_SDSub x,(i -' 1)) + (DigA_SDSub y,(i -' 1))),k;
DigA_SDSub x,i is Element of k -SD_Sub by A1, RADIX_3:19;
then A2: DigA_SDSub x,i in k -SD_Sub ;
A3: k -SD_Sub c= k -SD by A1, RADIX_3:5;
DigA_SDSub y,i is Element of k -SD_Sub by A1, RADIX_3:19;
then SDSub_Add_Data ((DigA_SDSub x,i) + (DigA_SDSub y,i)),k in k -SD_Sub_S by A1, A2, A3, RADIX_3:20;
then A4: ( SDSub_Add_Data ((DigA_SDSub x,i) + (DigA_SDSub y,i)),k >= - (Radix (k -' 1)) & SDSub_Add_Data ((DigA_SDSub x,i) + (DigA_SDSub y,i)),k <= (Radix (k -' 1)) - 1 ) by Lm1;
A5: ( - 1 <= SDSub_Add_Carry ((DigA_SDSub x,(i -' 1)) + (DigA_SDSub y,(i -' 1))),k & SDSub_Add_Carry ((DigA_SDSub x,(i -' 1)) + (DigA_SDSub y,(i -' 1))),k <= 1 ) by A1, RADIX_3:13;
then A6: (- (Radix (k -' 1))) + (- 1) <= (SDSub_Add_Data ((DigA_SDSub x,i) + (DigA_SDSub y,i)),k) + (SDSub_Add_Carry ((DigA_SDSub x,(i -' 1)) + (DigA_SDSub y,(i -' 1))),k) by A4, XREAL_1:9;
A7: (SDSub_Add_Data ((DigA_SDSub x,i) + (DigA_SDSub y,i)),k) + (SDSub_Add_Carry ((DigA_SDSub x,(i -' 1)) + (DigA_SDSub y,(i -' 1))),k) <= ((Radix (k -' 1)) - 1) + 1 by A4, A5, XREAL_1:9;
A8: (SDSub_Add_Data ((DigA_SDSub x,i) + (DigA_SDSub y,i)),k) + (SDSub_Add_Carry ((DigA_SDSub x,(i -' 1)) + (DigA_SDSub y,(i -' 1))),k) is Element of INT by INT_1:def 2;
k -SD_Sub = { w where w is Element of INT : ( w >= (- (Radix (k -' 1))) - 1 & w <= Radix (k -' 1) ) } by RADIX_3:def 2;
then (SDSub_Add_Data ((DigA_SDSub x,i) + (DigA_SDSub y,i)),k) + (SDSub_Add_Carry ((DigA_SDSub x,(i -' 1)) + (DigA_SDSub y,(i -' 1))),k) in k -SD_Sub by A6, A7, A8;
hence (SDSub_Add_Data ((DigA_SDSub x,i) + (DigA_SDSub y,i)),k) + (SDSub_Add_Carry ((DigA_SDSub x,(i -' 1)) + (DigA_SDSub y,(i -' 1))),k) is Element of k -SD_Sub ; :: thesis: verum