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:237
.= (2 to_power 1) * (2 to_power (k -' 1)) by POWER:32
.= 2 * (Radix (k -' 1)) by POWER:30
.= (Radix (k -' 1)) + (Radix (k -' 1)) ;
hence Radix k = (Radix (k -' 1)) + (Radix (k -' 1)) ; :: thesis: verum