let k be Nat; :: thesis: ( k >= 2 implies SD_Add_Data ((Radix k),k) = 0 )
assume k >= 2 ; :: thesis: SD_Add_Data ((Radix k),k) = 0
then A1: SD_Add_Carry (Radix k) = 1 by Th10;
SD_Add_Data ((Radix k),k) = (Radix k) - ((SD_Add_Carry (Radix k)) * (Radix k)) by RADIX_1:def 11
.= (Radix k) - (Radix k) by A1 ;
hence SD_Add_Data ((Radix k),k) = 0 ; :: thesis: verum