for L being non empty multLoopStr st L is well-unital holds
1. L = 1_ L by Lm1;