hereby :: thesis:

assume A1: V c= the_Vertices_of G ; :: thesis:
set E = { [(the_Edges_of G),v] where v is Vertex of G : v in V } ;
deffunc H₁( object ) -> object = $1 `2 ;
consider f being Function such that
A2: ( dom f = { [(the_Edges_of G),v] where v is Vertex of G : v in V } & ( for x being object st x in { [(the_Edges_of G),v] where v is Vertex of G : v in V } holds
f . x = H₁(x) ) ) from FUNCT_1:sch 3();
set s = (the_Source_of G) +* f;
set t = (the_Target_of G) +* f;

now :: thesis:

let y be object ; :: thesis:

hereby :: thesis:

assume y in rng f ; :: thesis:
then consider x being object such that
A3: ( x in dom f & f . x = y ) by FUNCT_1:def 3;
consider v being Vertex of G such that
A4: ( x = [(the_Edges_of G),v] & v in V ) by A2, A3;
y = x `2 by A2, A3
.= v by A4 ;
hence y in V by A4; :: thesis:

end;

set x = [(the_Edges_of G),y];
assume y in V ; :: thesis:
then A5: [(the_Edges_of G),y] in dom f by A1, A2;
then f . [(the_Edges_of G),y] = [(the_Edges_of G),y] `2 by A2
.= y ;
hence y in rng f by A5, FUNCT_1:3; :: thesis:

end;

then A6: rng f = V by TARSKI:2;
A7: dom ((the_Source_of G) +* f) = (dom (the_Source_of G)) \/ (dom f) by FUNCT_4:def 1
.= (the_Edges_of G) \/ { [(the_Edges_of G),v] where v is Vertex of G : v in V } by A2, FUNCT_2:def 1 ;
A8: dom ((the_Target_of G) +* f) = (dom (the_Target_of G)) \/ (dom f) by FUNCT_4:def 1
.= (the_Edges_of G) \/ { [(the_Edges_of G),v] where v is Vertex of G : v in V } by A2, FUNCT_2:def 1 ;
A9: the_Edges_of G misses { [(the_Edges_of G),v] where v is Vertex of G : v in V }

proof

assume the_Edges_of G meets { [(the_Edges_of G),v] where v is Vertex of G : v in V } ; :: thesis:
then consider e being object such that
A10: ( e in the_Edges_of G & e in { [(the_Edges_of G),v] where v is Vertex of G : v in V } ) by XBOOLE_0:3;
reconsider e = e as set by TARSKI:1;
consider v being Vertex of G such that
A11: ( e = [(the_Edges_of G),v] & v in V ) by A10;
A12: the_Edges_of G in {(the_Edges_of G)} by TARSKI:def 1;
e = {{(the_Edges_of G),v},{(the_Edges_of G)}} by A11, TARSKI:def 5;
then {(the_Edges_of G)} in e by TARSKI:def 2;
hence contradiction by A10, A12, XREGULAR:7; :: thesis:

end;

( (rng (the_Source_of G)) \/ (rng f) c= (the_Vertices_of G) \/ V & (rng (the_Target_of G)) \/ (rng f) c= (the_Vertices_of G) \/ V ) by A6, XBOOLE_1:9;
then A13: ( (rng (the_Source_of G)) \/ (rng f) c= the_Vertices_of G & (rng (the_Target_of G)) \/ (rng f) c= the_Vertices_of G ) by A1, XBOOLE_1:12;
( rng ((the_Source_of G) +* f) c= (rng (the_Source_of G)) \/ (rng f) & rng ((the_Target_of G) +* f) c= (rng (the_Target_of G)) \/ (rng f) ) by FUNCT_4:17;
then A14: ( rng ((the_Source_of G) +* f) c= the_Vertices_of G & rng ((the_Target_of G) +* f) c= the_Vertices_of G ) by A13, XBOOLE_1:1;
then reconsider s = (the_Source_of G) +* f as Function of ((the_Edges_of G) \/ { [(the_Edges_of G),v] where v is Vertex of G : v in V } ),(the_Vertices_of G) by A7, FUNCT_2:2;
reconsider t = (the_Target_of G) +* f as Function of ((the_Edges_of G) \/ { [(the_Edges_of G),v] where v is Vertex of G : v in V } ),(the_Vertices_of G) by A8, A14, FUNCT_2:2;
set H = createGraph ((the_Vertices_of G),((the_Edges_of G) \/ { [(the_Edges_of G),v] where v is Vertex of G : v in V } ),s,t);
A15: ( the_Edges_of G c= the_Edges_of (createGraph ((the_Vertices_of G),((the_Edges_of G) \/ { [(the_Edges_of G),v] where v is Vertex of G : v in V } ),s,t)) & the_Vertices_of G = the_Vertices_of (createGraph ((the_Vertices_of G),((the_Edges_of G) \/ { [(the_Edges_of G),v] where v is Vertex of G : v in V } ),s,t)) ) by XBOOLE_1:7;

now :: thesis:

let e be set ; :: thesis:
assume A16: e in the_Edges_of G ; :: thesis:
then e in (the_Edges_of G) \/ { [(the_Edges_of G),v] where v is Vertex of G : v in V } by XBOOLE_0:def 3;
then A17: not e in dom f by A2, A9, A16, XBOOLE_0:5;
hence (the_Source_of G) . e = (the_Source_of (createGraph ((the_Vertices_of G),((the_Edges_of G) \/ { [(the_Edges_of G),v] where v is Vertex of G : v in V } ),s,t))) . e by FUNCT_4:11; :: thesis:
thus (the_Target_of G) . e = (the_Target_of (createGraph ((the_Vertices_of G),((the_Edges_of G) \/ { [(the_Edges_of G),v] where v is Vertex of G : v in V } ),s,t))) . e by A17, FUNCT_4:11; :: thesis:

end;

then reconsider H = createGraph ((the_Vertices_of G),((the_Edges_of G) \/ { [(the_Edges_of G),v] where v is Vertex of G : v in V } ),s,t) as Supergraph of G by A15, GLIB_006:def 9;
take H = H; :: thesis:
thus the_Vertices_of H = the_Vertices_of G ; :: thesis:

now :: thesis:

let x1, x2 be object ; :: thesis:
assume A19: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 ) ; :: thesis:
then consider v1 being Vertex of G such that
A20: ( x1 = [(the_Edges_of G),v1] & v1 in V ) by A2;
consider v2 being Vertex of G such that
A21: ( x2 = [(the_Edges_of G),v2] & v2 in V ) by A2, A19;
thus x1 = [(the_Edges_of G),([(the_Edges_of G),v1] `2)] by A20
.= [(the_Edges_of G),(f . x2)] by A2, A19, A20
.= [(the_Edges_of G),([(the_Edges_of G),v2] `2)] by A2, A19, A21
.= x2 by A21 ; :: thesis:

end;

then reconsider f = f as one-to-one Function by FUNCT_1:def 4;
take E = { [(the_Edges_of G),v] where v is Vertex of G : v in V } ; :: thesis:
take f = f; :: thesis:
thus ( E misses the_Edges_of G & the_Edges_of H = (the_Edges_of G) \/ E ) by A9; :: thesis:
thus ( dom f = E & rng f = V ) by A2, A6; :: thesis:
thus ( the_Source_of H = (the_Source_of G) +* f & the_Target_of H = (the_Target_of G) +* f ) ; :: thesis:

end;

assume not V c= the_Vertices_of G ; :: thesis:
take G ; :: thesis:
thus ( G is Supergraph of G & G == G ) by GLIB_006:61; :: thesis: