let k be Nat; :: thesis: for i1, i2 being Integer st 2 <= k & i1 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 implies (SDSub_Add_Data (i1,k)) + (SDSub_Add_Carry (i2,k)) in k -SD_Sub )
A1: SDSub_Add_Carry (i2,k) >= - 1 by Th12;
assume A2: ( 2 <= k & i1 in k -SD ) ; :: thesis: (SDSub_Add_Data (i1,k)) + (SDSub_Add_Carry (i2,k)) in k -SD_Sub
then SDSub_Add_Data (i1,k) >= - (Radix (k -' 1)) by Th13;
then A3: (SDSub_Add_Data (i1,k)) + (SDSub_Add_Carry (i2,k)) >= (- (Radix (k -' 1))) + (- 1) by A1, XREAL_1:7;
A4: SDSub_Add_Carry (i2,k) <= 1 by Th12;
SDSub_Add_Data (i1,k) <= (Radix (k -' 1)) - 1 by A2, Th13;
then A5: (SDSub_Add_Data (i1,k)) + (SDSub_Add_Carry (i2,k)) <= ((Radix (k -' 1)) - 1) + 1 by A4, XREAL_1:7;
(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 A3, A5; :: thesis: verum