:: deftheorem Def3 defines e.i.-valued FVALUAT1:def 3 :
for f being Relation holds
( f is e.i.-valued iff for x being set st x in rng f holds
x is ext-integer );