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 = 2 to_power ((k -' 1) + 1) by XREAL_1:235
.= (2 to_power 1) * (2 to_power (k -' 1)) by POWER:27
.= 2 * (Radix (k -' 1)) by POWER:25
.= (Radix (k -' 1)) + (Radix (k -' 1)) ;
hence Radix k = (Radix (k -' 1)) + (Radix (k -' 1)) ; :: thesis: verum