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

for x being Element of (ValuatRing v) holds x is Element of K

let v be Valuation of K; :: thesis: ( K is having_valuation implies for x being Element of (ValuatRing v) holds x is Element of K )

assume A1: K is having_valuation ; :: thesis: for x being Element of (ValuatRing v) holds x is Element of K

let x be Element of (ValuatRing v); :: thesis: x is Element of K

the carrier of (ValuatRing v) = NonNegElements v by A1, Def12;

then ( x in NonNegElements v & NonNegElements v c= the carrier of K ) by Th48;

hence x is Element of K ; :: thesis: verum

for x being Element of (ValuatRing v) holds x is Element of K

let v be Valuation of K; :: thesis: ( K is having_valuation implies for x being Element of (ValuatRing v) holds x is Element of K )

assume A1: K is having_valuation ; :: thesis: for x being Element of (ValuatRing v) holds x is Element of K

let x be Element of (ValuatRing v); :: thesis: x is Element of K

the carrier of (ValuatRing v) = NonNegElements v by A1, Def12;

then ( x in NonNegElements v & NonNegElements v c= the carrier of K ) by Th48;

hence x is Element of K ; :: thesis: verum