LenBSeq 0 = 1 by BINARI_6:def 1;
then Nat2BL . 0 = 1 -BinarySequence 0 by BINARI_6:def 2
.= <*0*> by BINARI_3:25, BINARI_6:4 ;
hence Nat2BL . 0 = <*0*> ; :: thesis: verum