theorem :: FIELD_15:47
for R being non degenerated unital doubleLoopStr
for n being non zero Nat
for a being Element of R holds LC (X^ (n,a)) = 1. R by Lm13;