let k be Nat; :: thesis: for i1, i2 being Integer st 2 <= k & i1 in k -SD & i2 in k -SD_Sub holds
SDSub_Add_Data ((i1 + i2),k) in k -SD_Sub_S
let i1, i2 be Integer; :: thesis: ( 2 <= k & i1 in k -SD & i2 in k -SD_Sub implies SDSub_Add_Data ((i1 + i2),k) in k -SD_Sub_S )
assume that
A1: 2 <= k and
A2: ( i1 in k -SD & i2 in k -SD_Sub ) ; :: thesis: SDSub_Add_Data ((i1 + i2),k) in k -SD_Sub_S
set z = i1 + i2;
( i1 <= (Radix k) - 1 & i2 <= Radix (k -' 1) ) by A2, Th1, RADIX_1:13;
then A3: i1 + i2 <= ((Radix k) - 1) + (Radix (k -' 1)) by XREAL_1:7;
( (- (Radix k)) + 1 <= i1 & (- (Radix (k -' 1))) - 1 <= i2 ) by A2, Th1, RADIX_1:13;
then A4: ((- (Radix k)) + 1) + ((- (Radix (k -' 1))) - 1) <= i1 + i2 by XREAL_1:7;
A5: ( SDSub_Add_Data ((i1 + i2),k) >= - (Radix (k -' 1)) & SDSub_Add_Data ((i1 + i2),k) <= (Radix (k -' 1)) - 1 )

proof

now :: thesis: ( ( i1 + i2 < - (Radix (k -' 1)) & SDSub_Add_Data ((i1 + i2),k) >= - (Radix (k -' 1)) & SDSub_Add_Data ((i1 + i2),k) <= (Radix (k -' 1)) - 1 ) or ( - (Radix (k -' 1)) <= i1 + i2 & i1 + i2 < Radix (k -' 1) & SDSub_Add_Data ((i1 + i2),k) >= - (Radix (k -' 1)) & SDSub_Add_Data ((i1 + i2),k) <= (Radix (k -' 1)) - 1 ) or ( Radix (k -' 1) <= i1 + i2 & SDSub_Add_Data ((i1 + i2),k) >= - (Radix (k -' 1)) & SDSub_Add_Data ((i1 + i2),k) <= (Radix (k -' 1)) - 1 ) )

per cases ( i1 + i2 < - (Radix (k -' 1)) or ( - (Radix (k -' 1)) <= i1 + i2 & i1 + i2 < Radix (k -' 1) ) or Radix (k -' 1) <= i1 + i2 ) ;

case A6: i1 + i2 < - (Radix (k -' 1)) ; :: thesis: ( SDSub_Add_Data ((i1 + i2),k) >= - (Radix (k -' 1)) & SDSub_Add_Data ((i1 + i2),k) <= (Radix (k -' 1)) - 1 )

then (i1 + i2) + 1 <= - (Radix (k -' 1)) by INT_1:7;
then i1 + i2 <= (- (Radix (k -' 1))) - 1 by XREAL_1:19;
then i1 + i2 <= (- (Radix (k -' 1))) + (- 1) ;
then i1 + i2 <= ((- (Radix k)) + (Radix (k -' 1))) + (- 1) by A1, Lm3, XXREAL_0:2;
then A7: i1 + i2 <= (- (Radix k)) + ((Radix (k -' 1)) + (- 1)) ;
(- (Radix (k -' 1))) + (- (Radix k)) <= (i1 + i2) + 0 by A4;
then A8: (- (Radix (k -' 1))) - 0 <= (i1 + i2) - (- (Radix k)) by XREAL_1:21;
SDSub_Add_Carry ((i1 + i2),k) = - 1 by A6, Def3;
hence ( SDSub_Add_Data ((i1 + i2),k) >= - (Radix (k -' 1)) & SDSub_Add_Data ((i1 + i2),k) <= (Radix (k -' 1)) - 1 ) by A8, A7, XREAL_1:20; :: thesis: verum

end;

case A9: ( - (Radix (k -' 1)) <= i1 + i2 & i1 + i2 < Radix (k -' 1) ) ; :: thesis: ( SDSub_Add_Data ((i1 + i2),k) >= - (Radix (k -' 1)) & SDSub_Add_Data ((i1 + i2),k) <= (Radix (k -' 1)) - 1 )

then ( SDSub_Add_Carry ((i1 + i2),k) = 0 & (i1 + i2) + 1 <= Radix (k -' 1) ) by Def3, INT_1:7;
hence ( SDSub_Add_Data ((i1 + i2),k) >= - (Radix (k -' 1)) & SDSub_Add_Data ((i1 + i2),k) <= (Radix (k -' 1)) - 1 ) by A9, XREAL_1:19; :: thesis: verum

end;

case A10: Radix (k -' 1) <= i1 + i2 ; :: thesis: ( SDSub_Add_Data ((i1 + i2),k) >= - (Radix (k -' 1)) & SDSub_Add_Data ((i1 + i2),k) <= (Radix (k -' 1)) - 1 )

then (Radix k) - (Radix (k -' 1)) <= i1 + i2 by A1, Lm2, XXREAL_0:2;
then A11: (Radix k) + (- (Radix (k -' 1))) <= i1 + i2 ;
A12: i1 + i2 <= (Radix k) + ((Radix (k -' 1)) - 1) by A3;
SDSub_Add_Carry ((i1 + i2),k) = 1 by A10, Def3;
hence ( SDSub_Add_Data ((i1 + i2),k) >= - (Radix (k -' 1)) & SDSub_Add_Data ((i1 + i2),k) <= (Radix (k -' 1)) - 1 ) by A11, A12, XREAL_1:19, XREAL_1:20; :: thesis: verum

end;

end;

end;

hence ( SDSub_Add_Data ((i1 + i2),k) >= - (Radix (k -' 1)) & SDSub_Add_Data ((i1 + i2),k) <= (Radix (k -' 1)) - 1 ) ; :: thesis: verum

end;

SDSub_Add_Data ((i1 + i2),k) is Element of INT by INT_1:def 2;
hence SDSub_Add_Data ((i1 + i2),k) in k -SD_Sub_S by A5; :: thesis: verum