theorem Th4: :: POLYNOM4:4

for L being non empty non degenerated multLoopStr_0 holds len (1_. L) = 1