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:39;
hence SDSub_Add_Carry 0 ,k = 0 by Def3; :: thesis: verum