let i1, i2 be Integer; :: thesis: for k being Nat st k >= 2 & i1 in k -SD & i2 in k -SD holds
( (- (Radix k)) + 2 <= SD_Add_Data (i1 + i2),k & SD_Add_Data (i1 + i2),k <= (Radix k) - 2 )
let k be Nat; :: thesis: ( k >= 2 & i1 in k -SD & i2 in k -SD implies ( (- (Radix k)) + 2 <= SD_Add_Data (i1 + i2),k & SD_Add_Data (i1 + i2),k <= (Radix k) - 2 ) )
assume A1: ( k >= 2 & i1 in k -SD & i2 in k -SD ) ; :: thesis: ( (- (Radix k)) + 2 <= SD_Add_Data (i1 + i2),k & SD_Add_Data (i1 + i2),k <= (Radix k) - 2 )
then A2: ( (- (Radix k)) + 1 <= i1 & i1 <= (Radix k) - 1 & (- (Radix k)) + 1 <= i2 & i2 <= (Radix k) - 1 ) by Th15;
set z = i1 + i2;
A3: ( ((- (Radix k)) + 1) + ((- (Radix k)) + 1) <= i1 + i2 & i1 + i2 <= ((Radix k) - 1) + ((Radix k) - 1) ) by A2, XREAL_1:9;

per cases ( i1 + i2 < - 2 or ( - 2 <= i1 + i2 & i1 + i2 <= 2 ) or i1 + i2 > 2 ) ;

suppose A4: i1 + i2 < - 2 ; :: thesis: ( (- (Radix k)) + 2 <= SD_Add_Data (i1 + i2),k & SD_Add_Data (i1 + i2),k <= (Radix k) - 2 )

then A5: SD_Add_Carry (i1 + i2) = - 1 by Def10;
((- (Radix k)) + 1) + (1 + (- (Radix k))) <= i1 + i2 by A2, XREAL_1:9;
then A6: ((- (Radix k)) + (1 + 1)) - (Radix k) <= i1 + i2 ;
(i1 + i2) + (Radix k) < (- 2) + (Radix k) by A4, XREAL_1:8;
hence ( (- (Radix k)) + 2 <= SD_Add_Data (i1 + i2),k & SD_Add_Data (i1 + i2),k <= (Radix k) - 2 ) by A5, A6, XREAL_1:22; :: thesis: verum

end;

suppose A7: ( - 2 <= i1 + i2 & i1 + i2 <= 2 ) ; :: thesis: ( (- (Radix k)) + 2 <= SD_Add_Data (i1 + i2),k & SD_Add_Data (i1 + i2),k <= (Radix k) - 2 )

then A8: SD_Add_Carry (i1 + i2) = 0 by Def10;
A9: Radix k >= 2 + 2 by A1, Lm1;
then A10: (Radix k) - 2 >= 2 by XREAL_1:21;
- (Radix k) <= - (2 + 2) by A9, XREAL_1:26;
then - (Radix k) <= (- 2) + (- 2) ;
then (- (Radix k)) - (- 2) <= - 2 by XREAL_1:22;
hence ( (- (Radix k)) + 2 <= SD_Add_Data (i1 + i2),k & SD_Add_Data (i1 + i2),k <= (Radix k) - 2 ) by A7, A8, A10, XXREAL_0:2; :: thesis: verum

end;

suppose A11: i1 + i2 > 2 ; :: thesis: ( (- (Radix k)) + 2 <= SD_Add_Data (i1 + i2),k & SD_Add_Data (i1 + i2),k <= (Radix k) - 2 )

then A12: SD_Add_Carry (i1 + i2) = 1 by Def10;
A13: i1 + i2 <= (((Radix k) - 1) - 1) + (Radix k) by A3;
(i1 + i2) - (Radix k) > 2 - (Radix k) by A11, XREAL_1:11;
hence ( (- (Radix k)) + 2 <= SD_Add_Data (i1 + i2),k & SD_Add_Data (i1 + i2),k <= (Radix k) - 2 ) by A12, A13, XREAL_1:22; :: thesis: verum

end;

end;