LenBSeq 4 = [\(log (2,4))/] + 1 by EXL2
.= [\2/] + 1 by POWER:def 3, POWER:60
.= 2 + 1 by INT_1:25
.= 3 ;
then Nat2BL . 4 = 3 -BinarySequence 4 by BINARI_6:def 2
.= (0* 2) ^ <*1*> by BINARI_3:28, POWER:60
.= <*0,0,1*> by BINARI_6:5, BINARI_6:4 ;
hence Nat2BL . 4 = <*0,0,1*> ; :: thesis: verum