take f = A --> 0.; :: thesis: f is e.i.-valued
let x be set ; :: according to FVALUAT1:def 3 :: thesis: ( x in rng f implies x is ext-integer )
rng f c= {0} by FUNCOP_1:13;
hence ( x in rng f implies x is ext-integer ) ; :: thesis: verum