theorem :: BINARI_3:36

for n being non zero Nat
for x being Tuple of n, BOOLEAN holds n -BinarySequence (Absval x) = x