theorem :: FIELD_16:30

for R being non degenerated unital doubleLoopStr
for a being Element of R
for n being non trivial Nat holds
( (X^ (n,R)) . 1 = - (1. R) & (X^ (n,R)) . n = 1. R & ( for m being Nat st m <> 1 & m <> n holds
(X^ (n,R)) . m = 0. R ) ) by Lm10, Lm11;