theorem :: BINARI_3:8

for n being Nat holds Rev (0* n) = 0* n