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