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

let x be object ; :: thesis: ( x in union (the_Edges_of S) implies x in dom (union (the_Target_of S)) )
assume x in union (the_Edges_of S) ; :: thesis: x in dom (union (the_Target_of S))
then consider E being set such that
A4: ( x in E & E in the_Edges_of S ) by TARSKI:def 4;
consider G being _Graph such that
A5: ( G in S & E = the_Edges_of G ) by A4, Def15;
A6: x in dom (the_Target_of G) by A4, A5, FUNCT_2:def 1;
the_Target_of G in the_Target_of S by A5, Def17;
then dom (the_Target_of G) c= dom (union (the_Target_of S)) by COMPUT_1:13;
hence x in dom (union (the_Target_of S)) by A6; :: thesis: verum

end;

then union (the_Edges_of S) c= dom (union (the_Target_of S)) by TARSKI:def 3;
hence union (the_Target_of S) is total by PARTFUN1:def 2, XBOOLE_0:def 10; :: thesis: verum