theorem :: VECTSP_2:27

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