let k be Nat; :: thesis: for i1, i2 being Integer st 2 <= k & i1 in k -SD & i2 in k -SD holds
(SDSub_Add_Data i1,k) + (SDSub_Add_Carry i2,k) in k -SD_Sub
let i1, i2 be Integer; :: thesis: ( 2 <= k & i1 in k -SD & i2 in k -SD implies (SDSub_Add_Data i1,k) + (SDSub_Add_Carry i2,k) in k -SD_Sub )
assume A1: ( 2 <= k & i1 in k -SD & i2 in k -SD ) ; :: thesis: (SDSub_Add_Data i1,k) + (SDSub_Add_Carry i2,k) in k -SD_Sub
then A2: ( SDSub_Add_Data i1,k >= - (Radix (k -' 1)) & SDSub_Add_Data i1,k <= (Radix (k -' 1)) - 1 ) by Th14;
A3: ( SDSub_Add_Carry i2,k >= - 1 & SDSub_Add_Carry i2,k <= 1 ) by A1, Th13;
then A4: (SDSub_Add_Data i1,k) + (SDSub_Add_Carry i2,k) >= (- (Radix (k -' 1))) + (- 1) by A2, XREAL_1:9;
A5: (SDSub_Add_Data i1,k) + (SDSub_Add_Carry i2,k) <= ((Radix (k -' 1)) - 1) + 1 by A2, A3, XREAL_1:9;
(SDSub_Add_Data i1,k) + (SDSub_Add_Carry i2,k) is Element of INT by INT_1:def 2;
hence (SDSub_Add_Data i1,k) + (SDSub_Add_Carry i2,k) in k -SD_Sub by A4, A5; :: thesis: verum