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