let G be Dsimple _Graph; :: thesis: ex f being one-to-one Function st
( dom f = the_Edges_of G & rng f c= [:(the_Vertices_of G),(the_Vertices_of G):] \ (id (the_Vertices_of G)) & ( for e being object st e in dom f holds
f . e = [((the_Source_of G) . e),((the_Target_of G) . e)] ) )
consider f being one-to-one Function such that
A1: ( dom f = the_Edges_of G & rng f c= [:(the_Vertices_of G),(the_Vertices_of G):] ) and
A2: for e being object st e in dom f holds
f . e = [((the_Source_of G) . e),((the_Target_of G) . e)] by Th1;
take f ; :: thesis: ( dom f = the_Edges_of G & rng f c= [:(the_Vertices_of G),(the_Vertices_of G):] \ (id (the_Vertices_of G)) & ( for e being object st e in dom f holds
f . e = [((the_Source_of G) . e),((the_Target_of G) . e)] ) )
rng f misses id (the_Vertices_of G)
proof
assume rng f meets id (the_Vertices_of G) ; :: thesis: contradiction
then consider y being object such that
A3: ( y in rng f & y in id (the_Vertices_of G) ) by XBOOLE_0:3;
consider x being object such that
A4: ( x in dom f & f . x = y ) by A3, FUNCT_1:def 3;
y = [((the_Source_of G) . x),((the_Target_of G) . x)] by A2, A4;
then (the_Source_of G) . x = (the_Target_of G) . x by A3, RELAT_1:def 10;
hence contradiction by A1, A4, GLIB_000:def 18; :: thesis: verum
end;
hence ( dom f = the_Edges_of G & rng f c= [:(the_Vertices_of G),(the_Vertices_of G):] \ (id (the_Vertices_of G)) & ( for e being object st e in dom f holds
f . e = [((the_Source_of G) . e),((the_Target_of G) . e)] ) ) by A1, A2, XBOOLE_1:86; :: thesis: verum