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