theorem :: HURWITZ2:8

for L being non empty multLoopStr_0 holds
( even_part (1_. L) = 1_. L & odd_part (1_. L) = 0_. L )