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

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