let G be non-Dmulti _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):] & ( for e being object st e in dom f holds
f . e = [((the_Source_of G) . e),((the_Target_of G) . e)] ) )
deffunc H₁( object ) -> object = [((the_Source_of G) . $1),((the_Target_of G) . $1)];
consider f being Function such that
A1: dom f = the_Edges_of G and
A2: for e being object st e in the_Edges_of G holds
f . e = H₁(e) from FUNCT_1:sch 3();

now :: thesis: for x1, x2 being object st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds
x1 = x2

let x1, x2 be object ; :: thesis: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 implies x1 = x2 )
assume A3: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 ) ; :: thesis: x1 = x2
then ( f . x1 = [((the_Source_of G) . x1),((the_Target_of G) . x1)] & f . x2 = [((the_Source_of G) . x2),((the_Target_of G) . x2)] ) by A1, A2;
then A4: ( (the_Source_of G) . x1 = (the_Source_of G) . x2 & (the_Target_of G) . x1 = (the_Target_of G) . x2 ) by A3, XTUPLE_0:1;
( x1 DJoins (the_Source_of G) . x1,(the_Target_of G) . x1,G & x2 DJoins (the_Source_of G) . x2,(the_Target_of G) . x2,G ) by A1, A3, GLIB_000:def 14;
hence x1 = x2 by A4, GLIB_000:def 21; :: thesis: verum

end;

then reconsider f = f as one-to-one Function by FUNCT_1:def 4;
take f ; :: thesis: ( dom f = the_Edges_of G & rng f c= [:(the_Vertices_of G),(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)] ) )
thus dom f = the_Edges_of G by A1; :: thesis: ( rng f c= [:(the_Vertices_of G),(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)] ) )

now :: thesis: for y being object st y in rng f holds
y in [:(the_Vertices_of G),(the_Vertices_of G):]

let y be object ; :: thesis: ( y in rng f implies y in [:(the_Vertices_of G),(the_Vertices_of G):] )
assume y in rng f ; :: thesis: y in [:(the_Vertices_of G),(the_Vertices_of G):]
then consider x being object such that
A5: ( x in dom f & f . x = y ) by FUNCT_1:def 3;
A6: y = [((the_Source_of G) . x),((the_Target_of G) . x)] by A1, A2, A5;
x Joins (the_Source_of G) . x,(the_Target_of G) . x,G by A1, A5, GLIB_000:def 13;
then ( (the_Source_of G) . x is Vertex of G & (the_Target_of G) . x is Vertex of G ) by GLIB_000:13;
hence y in [:(the_Vertices_of G),(the_Vertices_of G):] by A6, ZFMISC_1:def 2; :: thesis: verum

end;

hence rng f c= [:(the_Vertices_of G),(the_Vertices_of G):] by TARSKI:def 3; :: thesis: for e being object st e in dom f holds
f . e = [((the_Source_of G) . e),((the_Target_of G) . e)]
thus 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; :: thesis: verum