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 & v . a = 0 holds

( a is Element of (ValuatRing v) & a " is Element of (ValuatRing v) )

let a be Element of K; :: thesis: for v being Valuation of K st K is having_valuation & v . a = 0 holds

( a is Element of (ValuatRing v) & a " is Element of (ValuatRing v) )

let v be Valuation of K; :: thesis: ( K is having_valuation & v . a = 0 implies ( a is Element of (ValuatRing v) & a " is Element of (ValuatRing v) ) )

assume A1: K is having_valuation ; :: thesis: ( not v . a = 0 or ( a is Element of (ValuatRing v) & a " is Element of (ValuatRing v) ) )

assume A2: v . a = 0 ; :: thesis: ( a is Element of (ValuatRing v) & a " is Element of (ValuatRing v) )

thus a is Element of (ValuatRing v) by A1, A2, Th52; :: thesis: a " is Element of (ValuatRing v)

a <> 0. K by A1, A2, Def8;

then v . (a ") = - (v . a) by A1, Th21;

hence a " is Element of (ValuatRing v) by A1, A2, Th52; :: thesis: verum

for v being Valuation of K st K is having_valuation & v . a = 0 holds

( a is Element of (ValuatRing v) & a " is Element of (ValuatRing v) )

let a be Element of K; :: thesis: for v being Valuation of K st K is having_valuation & v . a = 0 holds

( a is Element of (ValuatRing v) & a " is Element of (ValuatRing v) )

let v be Valuation of K; :: thesis: ( K is having_valuation & v . a = 0 implies ( a is Element of (ValuatRing v) & a " is Element of (ValuatRing v) ) )

assume A1: K is having_valuation ; :: thesis: ( not v . a = 0 or ( a is Element of (ValuatRing v) & a " is Element of (ValuatRing v) ) )

assume A2: v . a = 0 ; :: thesis: ( a is Element of (ValuatRing v) & a " is Element of (ValuatRing v) )

thus a is Element of (ValuatRing v) by A1, A2, Th52; :: thesis: a " is Element of (ValuatRing v)

a <> 0. K by A1, A2, Def8;

then v . (a ") = - (v . a) by A1, Th21;

hence a " is Element of (ValuatRing v) by A1, A2, Th52; :: thesis: verum