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

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