theorem :: FIELD_15:45

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