let k be Nat; :: thesis: SDSub_Add_Carry (0,k) = 0
set x = 0 ;
( Radix (k -' 1) <> 0 & - (Radix (k -' 1)) <= 0 - 0 ) by POWER:34;
hence SDSub_Add_Carry (0,k) = 0 by Def3; :: thesis: verum