let G be non-multi _Graph; :: thesis: ex f being one-to-one Function st
( dom f = the_Edges_of G & rng f c= (2Set (the_Vertices_of G)) \/ (singletons (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 ) -> set = {((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 b₁ = b₂ )
assume A3: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 ) ; :: thesis: b₁ = b₂
then A4: ( 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;
A5: ( x1 Joins (the_Source_of G) . x1,(the_Target_of G) . x1,G & x2 Joins (the_Source_of G) . x2,(the_Target_of G) . x2,G ) by A1, A3, GLIB_000:def 13;

per cases ( ( (the_Source_of G) . x1 = (the_Source_of G) . x2 & (the_Target_of G) . x1 = (the_Target_of G) . x2 ) or ( (the_Source_of G) . x1 = (the_Target_of G) . x2 & (the_Target_of G) . x1 = (the_Source_of G) . x2 ) ) by A3, A4, ZFMISC_1:22;

suppose ( (the_Source_of G) . x1 = (the_Source_of G) . x2 & (the_Target_of G) . x1 = (the_Target_of G) . x2 ) ; :: thesis: b₁ = b₂

hence x1 = x2 by A5, GLIB_000:def 20; :: thesis: verum

end;

suppose ( (the_Source_of G) . x1 = (the_Target_of G) . x2 & (the_Target_of G) . x1 = (the_Source_of G) . x2 ) ; :: thesis: b₁ = b₂

then x2 Joins (the_Source_of G) . x1,(the_Target_of G) . x1,G by A5, GLIB_000:14;
hence x1 = x2 by A5, GLIB_000:def 20; :: thesis: verum

end;

end;

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= (2Set (the_Vertices_of G)) \/ (singletons (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= (2Set (the_Vertices_of G)) \/ (singletons (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)} ) )
for y being object st y in rng f holds
y in (2Set (the_Vertices_of G)) \/ (singletons (the_Vertices_of G))

proof

let y be object ; :: thesis: ( y in rng f implies y in (2Set (the_Vertices_of G)) \/ (singletons (the_Vertices_of G)) )
assume y in rng f ; :: thesis: y in (2Set (the_Vertices_of G)) \/ (singletons (the_Vertices_of G))
then consider x being object such that
A6: ( x in dom f & f . x = y ) by FUNCT_1:def 3;
reconsider z = y as set by TARSKI:1;
A7: y = {((the_Source_of G) . x),((the_Target_of G) . x)} by A1, A2, A6;
x Joins (the_Source_of G) . x,(the_Target_of G) . x,G by A1, A6, GLIB_000:def 13;
then A8: ( (the_Source_of G) . x is Vertex of G & (the_Target_of G) . x is Vertex of G ) by GLIB_000:13;

per cases ( (the_Source_of G) . x = (the_Target_of G) . x or (the_Source_of G) . x <> (the_Target_of G) . x ) ;

suppose (the_Source_of G) . x = (the_Target_of G) . x ; :: thesis: y in (2Set (the_Vertices_of G)) \/ (singletons (the_Vertices_of G))

then y = {((the_Source_of G) . x)} by A7, ENUMSET1:29;
then ( z c= the_Vertices_of G & z is 1 -element ) by A8, ZFMISC_1:31;
then z in singletons (the_Vertices_of G) ;
hence y in (2Set (the_Vertices_of G)) \/ (singletons (the_Vertices_of G)) by XBOOLE_0:def 3; :: thesis: verum

end;

suppose (the_Source_of G) . x <> (the_Target_of G) . x ; :: thesis: y in (2Set (the_Vertices_of G)) \/ (singletons (the_Vertices_of G))

then ( z c= the_Vertices_of G & card z = 2 ) by A7, A8, ZFMISC_1:32, CARD_2:57;
then z in TWOELEMENTSETS (the_Vertices_of G) ;
hence y in (2Set (the_Vertices_of G)) \/ (singletons (the_Vertices_of G)) by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

hence rng f c= (2Set (the_Vertices_of G)) \/ (singletons (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