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

vp v is prime

let v be Valuation of K; :: thesis: ( K is having_valuation implies vp v is prime )

assume A1: K is having_valuation ; :: thesis: vp v is prime

hence vp v is proper by Th76; :: according to RING_1:def 2 :: thesis: vp v is V266( ValuatRing v)

let a, b be Element of (ValuatRing v); :: according to RING_1:def 1 :: thesis: ( not a * b in vp v or a in vp v or b in vp v )

assume A2: a * b in vp v ; :: thesis: ( a in vp v or b in vp v )

assume not a in vp v ; :: thesis: b in vp v

then A3: v . a = 0 by A1, Th77;

assume A4: not b in vp v ; :: thesis: contradiction

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

A5: a * b = x * y by A1, Th55;

A6: v . y = 0 by A1, A4, Th77;

v . (x * y) = (v . x) + (v . y) by A1, Def8

.= 0 by A3, A6 ;

hence contradiction by A1, A2, A5, Th61; :: thesis: verum

vp v is prime

let v be Valuation of K; :: thesis: ( K is having_valuation implies vp v is prime )

assume A1: K is having_valuation ; :: thesis: vp v is prime

hence vp v is proper by Th76; :: according to RING_1:def 2 :: thesis: vp v is V266( ValuatRing v)

let a, b be Element of (ValuatRing v); :: according to RING_1:def 1 :: thesis: ( not a * b in vp v or a in vp v or b in vp v )

assume A2: a * b in vp v ; :: thesis: ( a in vp v or b in vp v )

assume not a in vp v ; :: thesis: b in vp v

then A3: v . a = 0 by A1, Th77;

assume A4: not b in vp v ; :: thesis: contradiction

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

A5: a * b = x * y by A1, Th55;

A6: v . y = 0 by A1, A4, Th77;

v . (x * y) = (v . x) + (v . y) by A1, Def8

.= 0 by A3, A6 ;

hence contradiction by A1, A2, A5, Th61; :: thesis: verum