theorem :: NTALGO_2:2

LenBSeq 0 = 1 by BINARI_6:def 1;