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

Pgenerator v is Element of (ValuatRing v)

let v be Valuation of K; :: thesis: ( K is having_valuation implies Pgenerator v is Element of (ValuatRing v) )

set a = Pgenerator v;

set l = least-positive (rng v);

assume A1: K is having_valuation ; :: thesis: Pgenerator v is Element of (ValuatRing v)

then A2: Pgenerator v = the Element of v " {(least-positive (rng v))} by Def9;

least-positive (rng v) in rng v by A1, Lm5;

then {(least-positive (rng v))} c= rng v by ZFMISC_1:31;

then not v " {(least-positive (rng v))} is empty by RELAT_1:139;

then v . (Pgenerator v) in {(least-positive (rng v))} by A2, FUNCT_1:def 7;

then v . (Pgenerator v) = least-positive (rng v) by TARSKI:def 1;

hence Pgenerator v is Element of (ValuatRing v) by A1, Th52; :: thesis: verum

Pgenerator v is Element of (ValuatRing v)

let v be Valuation of K; :: thesis: ( K is having_valuation implies Pgenerator v is Element of (ValuatRing v) )

set a = Pgenerator v;

set l = least-positive (rng v);

assume A1: K is having_valuation ; :: thesis: Pgenerator v is Element of (ValuatRing v)

then A2: Pgenerator v = the Element of v " {(least-positive (rng v))} by Def9;

least-positive (rng v) in rng v by A1, Lm5;

then {(least-positive (rng v))} c= rng v by ZFMISC_1:31;

then not v " {(least-positive (rng v))} is empty by RELAT_1:139;

then v . (Pgenerator v) in {(least-positive (rng v))} by A2, FUNCT_1:def 7;

then v . (Pgenerator v) = least-positive (rng v) by TARSKI:def 1;

hence Pgenerator v is Element of (ValuatRing v) by A1, Th52; :: thesis: verum