theorem Th38: :: NIVEN:40

for L being non empty non degenerated doubleLoopStr
for z1, z2 being Element of L holds LC <%z1,z2,(1. L)%> = 1. L