:: deftheorem Def2 defines Nat2BL BINARI_6:def 2 :
for b₁ being Function of NAT,(BOOLEAN *) holds
( b₁ = Nat2BL iff for x being Element of NAT holds b₁ . x = (LenBSeq x) -BinarySequence x );