let n be Element of NAT ; :: thesis: ( n > 0 implies ( log 2,(2 * n) = 1 + (log 2,n) & log 2,(2 * n) = (log 2,n) + 1 ) )
assume n > 0 ; :: thesis: ( log 2,(2 * n) = 1 + (log 2,n) & log 2,(2 * n) = (log 2,n) + 1 )
hence log 2,(2 * n) = (log 2,2) + (log 2,n) by POWER:61
.= 1 + (log 2,n) by POWER:60 ;
:: thesis: log 2,(2 * n) = (log 2,n) + 1
hence log 2,(2 * n) = (log 2,n) + 1 ; :: thesis: verum