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 holds
( v . a = 0 iff (normal-valuation v) . a = 0 )
let a be Element of K; :: thesis: for v being Valuation of K st K is having_valuation holds
( v . a = 0 iff (normal-valuation v) . a = 0 )
let v be Valuation of K; :: thesis: ( K is having_valuation implies ( v . a = 0 iff (normal-valuation v) . a = 0 ) )
assume K is having_valuation ; :: thesis: ( v . a = 0 iff (normal-valuation v) . a = 0 )
then v . a = ((normal-valuation v) . a) * (least-positive (rng v)) by Def10;
hence ( v . a = 0 iff (normal-valuation v) . a = 0 ) ; :: thesis: verum