for L being non empty ZeroStr holds (0. L) | L = 0_. L by T6;