theorem LM0071: :: BINARI_6:8

for n being Nat
for x being Tuple of n + 1, BOOLEAN st x . (n + 1) = 1 holds
( 2 to_power n <= Absval x & Absval x < 2 to_power (n + 1) )