let n be Nat; :: thesis: for R being non degenerated unital doubleLoopStr holds LC (npoly (R,n)) = 1. R
let R be non degenerated unital doubleLoopStr ; :: thesis: LC (npoly (R,n)) = 1. R
set q = npoly (R,n);
A: n = deg (npoly (R,n)) by lem6
.= (len (npoly (R,n))) - 1 by HURWITZ:def 2 ;
then n + 1 = len (npoly (R,n)) ;
then (len (npoly (R,n))) -' 1 = n by A, XREAL_1:233, NAT_1:11;
hence LC (npoly (R,n)) = 1. R by Lm10; :: thesis: verum