theorem LM090: :: BINARI_6:28

for n being Nat
for x being Element of NAT
for y being Tuple of n, BOOLEAN st y = Nat2BL . x holds
( n = LenBSeq x & Absval y = x & Nat2BL . (Absval y) = y )