for n being Nat holds n -BinarySequence 0 = ZERO n