theorem :: RING_4:14

for L being non empty multLoopStr_0 holds (1. L) | L = 1_. L ;