theorem :: BINARI_4:34

for l, m being Nat ex x being Element of BOOLEAN st (m + 1) -BinarySequence l = (m -BinarySequence l) ^ <*x*>