now :: thesis: for x being object st x in dom (union (the_Target_of S)) holds
x in union (the_Edges_of S)

let x be object ; :: thesis: ( x in dom (union (the_Target_of S)) implies x in union (the_Edges_of S) )
set y = (union (the_Target_of S)) . x;
assume x in dom (union (the_Target_of S)) ; :: thesis: x in union (the_Edges_of S)
then [x,((union (the_Target_of S)) . x)] in union (the_Target_of S) by FUNCT_1:1;
then consider s being set such that
A9: ( [x,((union (the_Target_of S)) . x)] in s & s in the_Target_of S ) by TARSKI:def 4;
consider G being _Graph such that
A10: ( G in S & s = the_Target_of G ) by A9, Def17;
x in dom (the_Target_of G) by A9, A10, FUNCT_1:1;
then A11: x in the_Edges_of G ;
the_Edges_of G in the_Edges_of S by A10, Def15;
hence x in union (the_Edges_of S) by A11, TARSKI:def 4; :: thesis: verum

end;

hence union (the_Target_of S) is union (the_Edges_of S) -defined by TARSKI:def 3, RELAT_1:def 18; :: thesis: union (the_Target_of S) is union (the_Vertices_of S) -valued

now :: thesis: for y being object st y in rng (union (the_Target_of S)) holds
y in union (the_Vertices_of S)

let y be object ; :: thesis: ( y in rng (union (the_Target_of S)) implies y in union (the_Vertices_of S) )
assume y in rng (union (the_Target_of S)) ; :: thesis: y in union (the_Vertices_of S)
then consider x being object such that
A12: ( x in dom (union (the_Target_of S)) & (union (the_Target_of S)) . x = y ) by FUNCT_1:def 3;
[x,y] in union (the_Target_of S) by A12, FUNCT_1:1;
then consider t being set such that
A13: ( [x,y] in t & t in the_Target_of S ) by TARSKI:def 4;
consider G being _Graph such that
A14: ( G in S & t = the_Target_of G ) by A13, Def17;
A15: x in dom (the_Target_of G) by A13, A14, FUNCT_1:1;
then (the_Target_of G) . x = y by A12, A13, A14, COMPUT_1:13;
then y in rng (the_Target_of G) by A15, FUNCT_1:3;
then A16: y in the_Vertices_of G ;
the_Vertices_of G in the_Vertices_of S by A14, Def14;
hence y in union (the_Vertices_of S) by A16, TARSKI:def 4; :: thesis: verum

end;

hence union (the_Target_of S) is union (the_Vertices_of S) -valued by TARSKI:def 3, RELAT_1:def 19; :: thesis: verum