theorem :: IDEA_1:10

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