let k be Nat; :: thesis: ( 1 <= k implies (Radix k) - (Radix (k -' 1)) = Radix (k -' 1) )
assume 1 <= k ; :: thesis: (Radix k) - (Radix (k -' 1)) = Radix (k -' 1)
then (Radix k) + 0 = (Radix (k -' 1)) + (Radix (k -' 1)) by Lm1;
hence (Radix k) - (Radix (k -' 1)) = Radix (k -' 1) ; :: thesis: verum