for n being Nat
for K being non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative Field-like doubleLoopStr
for v being Valuation of K st K is having_valuation holds
for x being Element of (ValuatRing v) st x <> 0. K holds
(power K) . (x,n) <> 0. K