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