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

for v being Valuation of K st K is having_valuation holds

( v . a = v . b iff (normal-valuation v) . a = (normal-valuation v) . b )

let a, b be Element of K; :: thesis: for v being Valuation of K st K is having_valuation holds

( v . a = v . b iff (normal-valuation v) . a = (normal-valuation v) . b )

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

set f = normal-valuation v;

set l = least-positive (rng v);

assume A1: K is having_valuation ; :: thesis: ( v . a = v . b iff (normal-valuation v) . a = (normal-valuation v) . b )

then A2: least-positive (rng v) in REAL by Lm6;

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

hence ( v . a = v . b iff (normal-valuation v) . a = (normal-valuation v) . b ) by A2, XXREAL_3:68; :: thesis: verum

for v being Valuation of K st K is having_valuation holds

( v . a = v . b iff (normal-valuation v) . a = (normal-valuation v) . b )

let a, b be Element of K; :: thesis: for v being Valuation of K st K is having_valuation holds

( v . a = v . b iff (normal-valuation v) . a = (normal-valuation v) . b )

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

set f = normal-valuation v;

set l = least-positive (rng v);

assume A1: K is having_valuation ; :: thesis: ( v . a = v . b iff (normal-valuation v) . a = (normal-valuation v) . b )

then A2: least-positive (rng v) in REAL by Lm6;

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

hence ( v . a = v . b iff (normal-valuation v) . a = (normal-valuation v) . b ) by A2, XXREAL_3:68; :: thesis: verum