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

ValuatRing v is domRing-like

let v be Valuation of K; :: thesis: ( K is having_valuation implies ValuatRing v is domRing-like )

set R = ValuatRing v;

assume A1: K is having_valuation ; :: thesis: ValuatRing v is domRing-like

let x, y be Element of (ValuatRing v); :: according to VECTSP_2:def 1 :: thesis: ( not x * y = 0. (ValuatRing v) or x = 0. (ValuatRing v) or y = 0. (ValuatRing v) )

assume that

A2: x * y = 0. (ValuatRing v) and

A3: x <> 0. (ValuatRing v) ; :: thesis: y = 0. (ValuatRing v)

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

A4: 0. (ValuatRing v) = 0. K by A1, Def12;

A5: x1 * y1 = x * y by A1, Th55;

y1 = (x1 ") * (x1 * y1) by A3, A4, Lm7

.= 0. K by A2, A4, A5 ;

hence y = 0. (ValuatRing v) by A1, Def12; :: thesis: verum

ValuatRing v is domRing-like

let v be Valuation of K; :: thesis: ( K is having_valuation implies ValuatRing v is domRing-like )

set R = ValuatRing v;

assume A1: K is having_valuation ; :: thesis: ValuatRing v is domRing-like

let x, y be Element of (ValuatRing v); :: according to VECTSP_2:def 1 :: thesis: ( not x * y = 0. (ValuatRing v) or x = 0. (ValuatRing v) or y = 0. (ValuatRing v) )

assume that

A2: x * y = 0. (ValuatRing v) and

A3: x <> 0. (ValuatRing v) ; :: thesis: y = 0. (ValuatRing v)

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

A4: 0. (ValuatRing v) = 0. K by A1, Def12;

A5: x1 * y1 = x * y by A1, Th55;

y1 = (x1 ") * (x1 * y1) by A3, A4, Lm7

.= 0. K by A2, A4, A5 ;

hence y = 0. (ValuatRing v) by A1, Def12; :: thesis: verum