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 <= () - 1 & i2 <= Radix (k -' 1) ) by ;
then A3: i1 + i2 <= (() - 1) + (Radix (k -' 1)) by XREAL_1:7;
( (- ()) + 1 <= i1 & (- (Radix (k -' 1))) - 1 <= i2 ) by ;
then A4: ((- ()) + 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
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 -' 1))) + (- 1) by ;
then A7: i1 + i2 <= (- ()) + ((Radix (k -' 1)) + (- 1)) ;
(- (Radix (k -' 1))) + (- ()) <= (i1 + i2) + 0 by A4;
then A8: (- (Radix (k -' 1))) - 0 <= (i1 + i2) - (- ()) by XREAL_1:21;
SDSub_Add_Carry ((i1 + i2),k) = - 1 by ;
hence ( SDSub_Add_Data ((i1 + i2),k) >= - (Radix (k -' 1)) & SDSub_Add_Data ((i1 + i2),k) <= (Radix (k -' 1)) - 1 ) by ; :: 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 ;
hence ( SDSub_Add_Data ((i1 + i2),k) >= - (Radix (k -' 1)) & SDSub_Add_Data ((i1 + i2),k) <= (Radix (k -' 1)) - 1 ) by ; :: 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 ;
then A11: (Radix k) + (- (Radix (k -' 1))) <= i1 + i2 ;
A12: i1 + i2 <= () + ((Radix (k -' 1)) - 1) by A3;
SDSub_Add_Carry ((i1 + i2),k) = 1 by ;
hence ( SDSub_Add_Data ((i1 + i2),k) >= - (Radix (k -' 1)) & SDSub_Add_Data ((i1 + i2),k) <= (Radix (k -' 1)) - 1 ) by ; :: 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