let L be non empty non degenerated doubleLoopStr ; :: thesis: for z being Element of L holds LC <%z,(1. L)%> = 1. L
let z be Element of L; :: thesis: LC <%z,(1. L)%> = 1. L
len <%z,(1. L)%> = 2 by POLYNOM5:40;
hence LC <%z,(1. L)%> = 1. L by Lm1, POLYNOM5:38; :: thesis: verum