theorem :: BINARI_4:3
for m being Nat holds (0* m) + (0* m) = 0* m