set C1 = dom f;
set C2 = rng f;
defpred S₁[ set ] means ex y, z being set st
( $1 = [y,z] & [{y},z] in Trace f );
consider X being set such that
A3: for x being set holds
( x in X iff ( x in [:(union (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, z being set st
( x = [y,z] & [{y},z] in Trace f ) )
let x be set ; :: thesis: ( x in X iff ex y, z being set st
( x = [y,z] & [{y},z] in Trace f ) )

now

given y, z being set such that A4: ( x = [y,z] & [{y},z] in Trace f ) ; :: thesis: x in [:(union (dom f)),(union (rng f)):]
A5: ( {y} in dom f & z in f . {y} ) by A4, Th32;
then ( f . {y} in rng f & y in {y} ) by FUNCT_1:def 5, TARSKI:def 1;
then ( y in union (dom f) & z in union (rng f) ) by A5, TARSKI:def 4;
hence x in [:(union (dom f)),(union (rng f)):] by A4, ZFMISC_1:106; :: thesis: verum

end;

hence ( x in X iff ex y, z being set st
( x = [y,z] & [{y},z] in Trace f ) ) by A3; :: thesis: verum