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 that
A1: k >= 2 and
A2: ( 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 )
A3: ( (- (Radix k)) + 1 <= i1 & (- (Radix k)) + 1 <= i2 ) by A2, Th12;
set z = i1 + i2;
( i1 <= (Radix k) - 1 & i2 <= (Radix k) - 1 ) by A2, Th12;
then A4: i1 + i2 <= ((Radix k) - 1) + ((Radix k) - 1) by XREAL_1:7;

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

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

((- (Radix k)) + 1) + (1 + (- (Radix k))) <= i1 + i2 by A3, XREAL_1:7;
then A6: ((- (Radix k)) + (1 + 1)) - (Radix k) <= i1 + i2 ;
( SD_Add_Carry (i1 + i2) = - 1 & (i1 + i2) + (Radix k) < (- 2) + (Radix k) ) by A5, Def10, XREAL_1:6;
hence ( (- (Radix k)) + 2 <= SD_Add_Data ((i1 + i2),k) & SD_Add_Data ((i1 + i2),k) <= (Radix k) - 2 ) by A6, XREAL_1:20; :: 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 )

A8: Radix k >= 2 + 2 by A1, Lm1;
then A9: (Radix k) - 2 >= 2 by XREAL_1:19;
- (Radix k) <= - (2 + 2) by A8, XREAL_1:24;
then - (Radix k) <= (- 2) + (- 2) ;
then A10: (- (Radix k)) - (- 2) <= - 2 by XREAL_1:20;
SD_Add_Carry (i1 + i2) = 0 by A7, Def10;
hence ( (- (Radix k)) + 2 <= SD_Add_Data ((i1 + i2),k) & SD_Add_Data ((i1 + i2),k) <= (Radix k) - 2 ) by A7, A9, 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 )

A12: i1 + i2 <= (((Radix k) - 1) - 1) + (Radix k) by A4;
( SD_Add_Carry (i1 + i2) = 1 & (i1 + i2) - (Radix k) > 2 - (Radix k) ) by A11, Def10, XREAL_1:9;
hence ( (- (Radix k)) + 2 <= SD_Add_Data ((i1 + i2),k) & SD_Add_Data ((i1 + i2),k) <= (Radix k) - 2 ) by A12, XREAL_1:20; :: thesis: verum

end;

end;