DigA_SDSub (x,i) is Element of k -SD_Sub by A1, RADIX_3:18;
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:12;
A5: SDSub_Add_Carry (((DigA_SDSub (x,(i -' 1))) + (DigA_SDSub (y,(i -' 1)))),k) <= 1 by RADIX_3:12;
( k -SD_Sub c= k -SD & DigA_SDSub (y,i) is Element of k -SD_Sub ) by A1, A2, RADIX_3:4, RADIX_3:18;
then A6: SDSub_Add_Data (((DigA_SDSub (x,i)) + (DigA_SDSub (y,i))),k) in k -SD_Sub_S by A2, A3, RADIX_3:19;
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:7;
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:7;
( (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