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