for L being non empty ZeroStr holds <%(0. L),(0. L)%> = 0_. L