let n be Nat; :: thesis: 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

let K be non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative Field-like doubleLoopStr ; :: thesis: 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

let v be Valuation of K; :: thesis: ( K is having_valuation implies for x being Element of (ValuatRing v) st x <> 0. K holds

(power K) . (x,n) <> 0. K )

assume A1: K is having_valuation ; :: thesis: for x being Element of (ValuatRing v) st x <> 0. K holds

(power K) . (x,n) <> 0. K

let x be Element of (ValuatRing v); :: thesis: ( x <> 0. K implies (power K) . (x,n) <> 0. K )

reconsider y = x as Element of K by A1, Th51;

(power K) . (y,n) = y |^ n ;

hence ( x <> 0. K implies (power K) . (x,n) <> 0. K ) by Th16; :: thesis: verum

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

let K be non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative Field-like doubleLoopStr ; :: thesis: 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

let v be Valuation of K; :: thesis: ( K is having_valuation implies for x being Element of (ValuatRing v) st x <> 0. K holds

(power K) . (x,n) <> 0. K )

assume A1: K is having_valuation ; :: thesis: for x being Element of (ValuatRing v) st x <> 0. K holds

(power K) . (x,n) <> 0. K

let x be Element of (ValuatRing v); :: thesis: ( x <> 0. K implies (power K) . (x,n) <> 0. K )

reconsider y = x as Element of K by A1, Th51;

(power K) . (y,n) = y |^ n ;

hence ( x <> 0. K implies (power K) . (x,n) <> 0. K ) by Th16; :: thesis: verum