theorem :: BINARI_4:3

for m being Nat holds (0* m) + (0* m) = 0* m