take f = 0 --> 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

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