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

now :: thesis: ( ex y, z being object st
( x = [y,z] & [{y},z] in Trace f ) implies x in [:(union (dom f)),(union (rng f)):] )

given y, z being object such that A4: x = [y,z] and
A5: [{y},z] in Trace f ; :: thesis: x in [:(union (dom f)),(union (rng f)):]
A6: {y} in dom f by A5, Th31;
then A7: f . {y} in rng f by FUNCT_1:def 3;
z in f . {y} by A5, Th31;
then A8: z in union (rng f) by A7, TARSKI:def 4;
y in {y} by TARSKI:def 1;
then y in union (dom f) by A6, TARSKI:def 4;
hence x in [:(union (dom f)),(union (rng f)):] by A4, A8, ZFMISC_1:87; :: thesis: verum

end;

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