for x being Element of NAT holds Nat2BL . x = (LenBSeq x) -BinarySequence x by Def2;
hence Nat2BL is one-to-one by LM030; :: thesis: verum