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
ValuatRing (normal-valuation v) = ValuatRing v
let v be Valuation of K; :: thesis: ( K is having_valuation implies ValuatRing (normal-valuation v) = ValuatRing v )
assume A1: K is having_valuation ; :: thesis: ValuatRing (normal-valuation v) = ValuatRing v
set f = normal-valuation v;
set R = ValuatRing v;
set S = ValuatRing (normal-valuation v);
A2: the carrier of (ValuatRing (normal-valuation v)) = NonNegElements (normal-valuation v) by A1, Def12;
A3: NonNegElements (normal-valuation v) = NonNegElements v by A1, Th82;
A4: the addF of (ValuatRing v) = the addF of K | [:(NonNegElements v),(NonNegElements v):] by A1, Def12
.= the addF of (ValuatRing (normal-valuation v)) by A1, A3, Def12 ;
A5: the multF of (ValuatRing v) = the multF of K | [:(NonNegElements v),(NonNegElements v):] by A1, Def12
.= the multF of (ValuatRing (normal-valuation v)) by A1, A3, Def12 ;
A6: the ZeroF of (ValuatRing v) = 0. K by A1, Def12
.= the ZeroF of (ValuatRing (normal-valuation v)) by A1, Def12 ;
the OneF of (ValuatRing v) = 1. K by A1, Def12
.= the OneF of (ValuatRing (normal-valuation v)) by A1, Def12 ;
hence ValuatRing (normal-valuation v) = ValuatRing v by A3, A2, A4, A5, A6, A1, Def12; :: thesis: verum