let K be non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr ; for v being Valuation of K st K is having_valuation holds
vp v is prime
let v be Valuation of K; ( K is having_valuation implies vp v is prime )
assume A1:
K is having_valuation
; vp v is prime
hence
vp v is proper
by Th79; RING_1:def 2 vp v is V245( ValuatRing v)
let a, b be Element of (ValuatRing v); RING_1:def 1 ( not a * b in vp v or a in vp v or b in vp v )
assume A2:
a * b in vp v
; ( a in vp v or b in vp v )
assume
not a in vp v
; b in vp v
then A3:
v . a = 0
by A1, Th80;
assume A4:
not b in vp v
; contradiction
reconsider x = a, y = b as Element of K by A1, Th54;
A5:
a * b = x * y
by A1, Th58;
A6:
v . y = 0
by A1, A4, Th80;
v . (x * y) =
(v . x) + (v . y)
by A1, Def10
.=
0
by A3, A6
;
hence
contradiction
by A1, A2, A5, Th64; verum