defpred S₁[ object ] 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 object 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 :: thesis: ( ex y being finite set ex z being set st
( x = [y,z] & y in dom f & z in f . y ) implies x in [:(dom f),(union (rng f)):] )

given y being finite set , z being set such that A2: x = [y,z] and
A3: y in dom f and
A4: z in f . y ; :: thesis: x in [:(dom f),(union (rng f)):]
f . y in rng f by A3, FUNCT_1:def 3;
then z in union (rng f) by A4, TARSKI:def 4;
hence x in [:(dom f),(union (rng f)):] by A2, A3, ZFMISC_1:87; :: 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