let k be Nat; 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; ( 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 )
; (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; verum