theorem Th35: :: BINARI_3:35

for n being non zero Nat
for k being Nat st k < 2 to_power n holds
Absval (n -BinarySequence k) = k