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