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