let x be Nat; :: thesis: x = Absval ((LenBSeq x) -BinarySequence x)
x < 2 to_power (LenBSeq x) by LM006;
hence x = Absval ((LenBSeq x) -BinarySequence x) by BINARI_3:35; :: thesis: verum