:: deftheorem Def8 defines Valuation FVALUAT1:def 8 :
for K being doubleLoopStr st K is having_valuation holds
for b₂ being e.i.-valued Function of K,ExtREAL holds
( b₂ is Valuation of K iff ( b₂ . (0. K) = +infty & ( for a being Element of K st a <> 0. K holds
b₂ . a in INT ) & ( for a, b being Element of K holds b₂ . (a * b) = (b₂ . a) + (b₂ . b) ) & ( for a being Element of K st 0 <= b₂ . a holds
0 <= b₂ . ((1. K) + a) ) & ex a being Element of K st
( b₂ . a <> 0 & b₂ . a <> +infty ) ) );