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
normal-valuation (normal-valuation v) = normal-valuation v
let v be Valuation of K; :: thesis: ( K is having_valuation implies normal-valuation (normal-valuation v) = normal-valuation v )
assume A1: K is having_valuation ; :: thesis: normal-valuation (normal-valuation v) = normal-valuation v
set f = normal-valuation v;
set g = normal-valuation (normal-valuation v);
let a be Element of K; :: according to FUNCT_2:def 8 :: thesis: (normal-valuation (normal-valuation v)) . a = (normal-valuation v) . a
set k = least-positive (rng (normal-valuation v));
A2: (normal-valuation v) . a = ((normal-valuation (normal-valuation v)) . a) * (least-positive (rng (normal-valuation v))) by A1, Def10;
(normal-valuation v) . (Pgenerator v) = 1 by A1, Th43;
then least-positive (rng (normal-valuation v)) = 1 by Th34;
hence (normal-valuation (normal-valuation v)) . a = (normal-valuation v) . a by A2, XXREAL_3:81; :: thesis: verum