let K be non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative Field-like doubleLoopStr ; for v being Valuation of K st K is having_valuation holds
ValuatRing (normal-valuation v) = ValuatRing v
let v be Valuation of K; ( K is having_valuation implies ValuatRing (normal-valuation v) = ValuatRing v )
assume A1:
K is having_valuation
; 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; verum