theorem Th28: :: UPROOTS:31

for L being non empty multLoopStr_0 holds 1_. L = <%(1. L)%>