let L be non empty non degenerated doubleLoopStr ; :: thesis: for z1, z2 being Element of L holds LC <%z1,z2,(1. L)%> = 1. L
let z1, z2 be Element of L; :: thesis: LC <%z1,z2,(1. L)%> = 1. L
len <%z1,z2,(1. L)%> = 3 by Th26;
hence LC <%z1,z2,(1. L)%> = 1. L by Lm2, Th23; :: thesis: verum