:: deftheorem Def10 defines normal-valuation FVALUAT1:def 10 :
for K being non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative Field-like doubleLoopStr
for v being Valuation of K st K is having_valuation holds
for b₃ being Valuation of K holds
( b₃ = normal-valuation v iff for a being Element of K holds v . a = (b₃ . a) * (least-positive (rng v)) );