theorem Th25: :: BINARI_3:25

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