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 not x in vp v holds

v . x = 0

let v be Valuation of K; :: thesis: ( K is having_valuation implies for x being Element of (ValuatRing v) st not x in vp v holds

v . x = 0 )

assume A1: K is having_valuation ; :: thesis: for x being Element of (ValuatRing v) st not x in vp v holds

v . x = 0

let x be Element of (ValuatRing v); :: thesis: ( not x in vp v implies v . x = 0 )

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

assume not x in vp v ; :: thesis: v . x = 0

then v . y <= 0 by A1, Th61;

hence v . x = 0 by A1, Th52; :: thesis: verum

for x being Element of (ValuatRing v) st not x in vp v holds

v . x = 0

let v be Valuation of K; :: thesis: ( K is having_valuation implies for x being Element of (ValuatRing v) st not x in vp v holds

v . x = 0 )

assume A1: K is having_valuation ; :: thesis: for x being Element of (ValuatRing v) st not x in vp v holds

v . x = 0

let x be Element of (ValuatRing v); :: thesis: ( not x in vp v implies v . x = 0 )

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

assume not x in vp v ; :: thesis: v . x = 0

then v . y <= 0 by A1, Th61;

hence v . x = 0 by A1, Th52; :: thesis: verum