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