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 a being Element of K

for v being Valuation of K st K is having_valuation & a is Element of (ValuatRing v) holds

(power K) . (a,n) is Element of (ValuatRing v)

let K be non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative Field-like doubleLoopStr ; :: thesis: for a being Element of K

for v being Valuation of K st K is having_valuation & a is Element of (ValuatRing v) holds

(power K) . (a,n) is Element of (ValuatRing v)

let a be Element of K; :: thesis: for v being Valuation of K st K is having_valuation & a is Element of (ValuatRing v) holds

(power K) . (a,n) is Element of (ValuatRing v)

let v be Valuation of K; :: thesis: ( K is having_valuation & a is Element of (ValuatRing v) implies (power K) . (a,n) is Element of (ValuatRing v) )

assume A1: K is having_valuation ; :: thesis: ( not a is Element of (ValuatRing v) or (power K) . (a,n) is Element of (ValuatRing v) )

assume a is Element of (ValuatRing v) ; :: thesis: (power K) . (a,n) is Element of (ValuatRing v)

then reconsider y = a as Element of (ValuatRing v) ;

reconsider n = n as Element of NAT by ORDINAL1:def 12;

(power (ValuatRing v)) . (y,n) is Element of (ValuatRing v) ;

hence (power K) . (a,n) is Element of (ValuatRing v) by A1, Th60; :: thesis: verum

for a being Element of K

for v being Valuation of K st K is having_valuation & a is Element of (ValuatRing v) holds

(power K) . (a,n) is Element of (ValuatRing v)

let K be non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative Field-like doubleLoopStr ; :: thesis: for a being Element of K

for v being Valuation of K st K is having_valuation & a is Element of (ValuatRing v) holds

(power K) . (a,n) is Element of (ValuatRing v)

let a be Element of K; :: thesis: for v being Valuation of K st K is having_valuation & a is Element of (ValuatRing v) holds

(power K) . (a,n) is Element of (ValuatRing v)

let v be Valuation of K; :: thesis: ( K is having_valuation & a is Element of (ValuatRing v) implies (power K) . (a,n) is Element of (ValuatRing v) )

assume A1: K is having_valuation ; :: thesis: ( not a is Element of (ValuatRing v) or (power K) . (a,n) is Element of (ValuatRing v) )

assume a is Element of (ValuatRing v) ; :: thesis: (power K) . (a,n) is Element of (ValuatRing v)

then reconsider y = a as Element of (ValuatRing v) ;

reconsider n = n as Element of NAT by ORDINAL1:def 12;

(power (ValuatRing v)) . (y,n) is Element of (ValuatRing v) ;

hence (power K) . (a,n) is Element of (ValuatRing v) by A1, Th60; :: thesis: verum