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