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 <> 0. K & a is Element of (ValuatRing v) & a " is Element of (ValuatRing v) holds

v . a = 0

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

v . a = 0

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

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

assume that

A2: a <> 0. K and

A3: a is Element of (ValuatRing v) ; :: thesis: ( not a " is Element of (ValuatRing v) or v . a = 0 )

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

then 0 <= v . (a ") by A1, Th52;

then - (- (v . a)) <= - 0 by A1, A2, Th21;

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

for v being Valuation of K st K is having_valuation & a <> 0. K & a is Element of (ValuatRing v) & a " is Element of (ValuatRing v) holds

v . a = 0

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

v . a = 0

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

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

assume that

A2: a <> 0. K and

A3: a is Element of (ValuatRing v) ; :: thesis: ( not a " is Element of (ValuatRing v) or v . a = 0 )

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

then 0 <= v . (a ") by A1, Th52;

then - (- (v . a)) <= - 0 by A1, A2, Th21;

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