theorem Th34: :: POLYDIFF:34
for n being Nat
for L being non empty ZeroStr holds (0_. L) || n = 0_. L