now :: thesis: for y being set st y in rng (doms f) holds
y is finite

let y be set ; :: thesis: ( y in rng (doms f) implies y is finite )
assume y in rng (doms f) ; :: thesis: y is finite
then consider x being object such that
A1: ( x in dom (doms f) & y = (doms f) . x ) by FUNCT_1:def 3;
x in dom f by A1, FUNCT_6:def 2;
then A2: ( x in dom f & f . x is Function & y = proj1 (f . x) ) by A1, FUNCT_6:def 2;
thus y is finite by A2; :: thesis: verum

end;

hence doms f is finite-yielding ; :: thesis: verum