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

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