theorem Th3: :: POLYNOM4:3
for L being non empty ZeroStr holds len (0_. L) = 0