let x be Integer; :: thesis: for k being Nat holds
( - 1 <= SDSub_Add_Carry (x,k) & SDSub_Add_Carry (x,k) <= 1 )
let k be Nat; :: thesis: ( - 1 <= SDSub_Add_Carry (x,k) & SDSub_Add_Carry (x,k) <= 1 )

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

suppose x < - (Radix (k -' 1)) ; :: thesis: ( - 1 <= SDSub_Add_Carry (x,k) & SDSub_Add_Carry (x,k) <= 1 )

hence ( - 1 <= SDSub_Add_Carry (x,k) & SDSub_Add_Carry (x,k) <= 1 ) by Def3; :: thesis: verum

end;

suppose ( - (Radix (k -' 1)) <= x & x < Radix (k -' 1) ) ; :: thesis: ( - 1 <= SDSub_Add_Carry (x,k) & SDSub_Add_Carry (x,k) <= 1 )

hence ( - 1 <= SDSub_Add_Carry (x,k) & SDSub_Add_Carry (x,k) <= 1 ) by Def3; :: thesis: verum

end;

suppose x >= Radix (k -' 1) ; :: thesis: ( - 1 <= SDSub_Add_Carry (x,k) & SDSub_Add_Carry (x,k) <= 1 )

hence ( - 1 <= SDSub_Add_Carry (x,k) & SDSub_Add_Carry (x,k) <= 1 ) by Def3; :: thesis: verum

end;

end;