let K be non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative Field-like doubleLoopStr ; :: thesis: for a being Element of K

for v being Valuation of K st K is having_valuation & v . a = 1 holds

normal-valuation v = v

let a be Element of K; :: thesis: for v being Valuation of K st K is having_valuation & v . a = 1 holds

normal-valuation v = v

let v be Valuation of K; :: thesis: ( K is having_valuation & v . a = 1 implies normal-valuation v = v )

set f = normal-valuation v;

assume that

A1: K is having_valuation and

A2: v . a = 1 ; :: thesis: normal-valuation v = v

let a be Element of K; :: according to FUNCT_2:def 8 :: thesis: (normal-valuation v) . a = v . a

thus v . a = ((normal-valuation v) . a) * (least-positive (rng v)) by A1, Def10

.= ((normal-valuation v) . a) * 1 by A2, Th34

.= (normal-valuation v) . a by XXREAL_3:81 ; :: thesis: verum

for v being Valuation of K st K is having_valuation & v . a = 1 holds

normal-valuation v = v

let a be Element of K; :: thesis: for v being Valuation of K st K is having_valuation & v . a = 1 holds

normal-valuation v = v

let v be Valuation of K; :: thesis: ( K is having_valuation & v . a = 1 implies normal-valuation v = v )

set f = normal-valuation v;

assume that

A1: K is having_valuation and

A2: v . a = 1 ; :: thesis: normal-valuation v = v

let a be Element of K; :: according to FUNCT_2:def 8 :: thesis: (normal-valuation v) . a = v . a

thus v . a = ((normal-valuation v) . a) * (least-positive (rng v)) by A1, Def10

.= ((normal-valuation v) . a) * 1 by A2, Th34

.= (normal-valuation v) . a by XXREAL_3:81 ; :: thesis: verum