X1: 2 to_power 0 <= 1 by POWER:24;
1 < 2 to_power (0 + 1) ;
hence LenBSeq 1 = 1 by BINARI_6:def 1, X1; :: thesis: verum