defpred S₁[ set ] means ex y being finite set ex z being set st
( $1 = [y,z] & y in dom f & z in f . y );
consider X being set such that
A1: for x being set holds
( x in X iff ( x in [:(dom f),(union (rng f)):] & S₁[x] ) ) from XBOOLE_0:sch 1();
take X ; :: thesis: for x being set holds
( x in X iff ex y being finite set ex z being set st
( x = [y,z] & y in dom f & z in f . y ) )
let x be set ; :: thesis: ( x in X iff ex y being finite set ex z being set st
( x = [y,z] & y in dom f & z in f . y ) )

now

given y being finite set , z being set such that A2: ( x = [y,z] & y in dom f & z in f . y ) ; :: thesis: x in [:(dom f),(union (rng f)):]
f . y in rng f by A2, FUNCT_1:def 5;
then z in union (rng f) by A2, TARSKI:def 4;
hence x in [:(dom f),(union (rng f)):] by A2, ZFMISC_1:106; :: thesis: verum

end;

hence ( x in X iff ex y being finite set ex z being set st
( x = [y,z] & y in dom f & z in f . y ) ) by A1; :: thesis: verum