let n be Nat; ( 0 < n implies LenBSeq n = [\(log (2,n))/] + 1 )
assume
0 < n
; LenBSeq n = [\(log (2,n))/] + 1
then consider x being Nat such that
LCX:
( 2 to_power x <= n & n < 2 to_power (x + 1) & LenBSeq n = x + 1 )
by BINARI_6:def 1;
log (2,(2 to_power x)) = x
by POWER:def 3;
then LT1:
x <= log (2,n)
by LCX, ASYMPT_2:7;
log (2,(2 to_power (x + 1))) = x + 1
by POWER:def 3;
then
log (2,n) < x + 1
by LCX, POWER:57;
then
(log (2,n)) - 1 < (x + 1) - 1
by XREAL_1:14;
hence
LenBSeq n = [\(log (2,n))/] + 1
by LCX, LT1, INT_1:def 6; verum