let k be Nat; :: thesis: for i1 being Integer st 2 <= k & i1 in k -SD holds
( SDSub_Add_Data (i1,k) >= - (Radix (k -' 1)) & SDSub_Add_Data (i1,k) <= (Radix (k -' 1)) - 1 )
let i1 be Integer; :: thesis: ( 2 <= k & i1 in k -SD implies ( SDSub_Add_Data (i1,k) >= - (Radix (k -' 1)) & SDSub_Add_Data (i1,k) <= (Radix (k -' 1)) - 1 ) )
assume that
A1: 2 <= k and
A2: i1 in k -SD ; :: thesis: ( SDSub_Add_Data (i1,k) >= - (Radix (k -' 1)) & SDSub_Add_Data (i1,k) <= (Radix (k -' 1)) - 1 )
A3: ( (- (Radix k)) + 1 <= i1 & 1 <= k ) by A1, A2, RADIX_1:13, XXREAL_0:2;

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

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

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

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

end;

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

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

end;

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

i1 <= (Radix k) + (- 1) by A2, RADIX_1:13;
then A8: ( 0 - 1 <= (Radix (k -' 1)) - 1 & i1 - (Radix k) <= - 1 ) by XREAL_1:9, XREAL_1:20;
( SDSub_Add_Carry (i1,k) = 1 & (Radix (k -' 1)) + (- (Radix k)) <= i1 + (- (Radix k)) ) by A7, Def3, XREAL_1:6;
hence ( SDSub_Add_Data (i1,k) >= - (Radix (k -' 1)) & SDSub_Add_Data (i1,k) <= (Radix (k -' 1)) - 1 ) by A1, A8, Lm3, XXREAL_0:2; :: thesis: verum

end;

end;

end;

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