let G be non-Dmulti _Graph; 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 H1( 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 = H1(e)
from FUNCT_1:sch 3();
now for x1, x2 being object st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds
x1 = x2let x1,
x2 be
object ;
( 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 )
;
x1 = x2then
(
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;
verum end;
then reconsider f = f as one-to-one Function by FUNCT_1:def 4;
take
f
; ( 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; ( 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 for y being object st y in rng f holds
y in [:(the_Vertices_of G),(the_Vertices_of G):]let y be
object ;
( y in rng f implies y in [:(the_Vertices_of G),(the_Vertices_of G):] )assume
y in rng f
;
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;
verum end;
hence
rng f c= [:(the_Vertices_of G),(the_Vertices_of G):]
by TARSKI:def 3; 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; verum