theorem :: FIELD_16:32

for R being non degenerated unital doubleLoopStr
for n being non trivial Nat holds LC (X^ (n,R)) = 1. R by Lm13;