let G2 be _Graph; :: thesis: for v being object
for V being set
for G1 being addAdjVertexFromAll of G2,v,V
for v1 being object st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & v1 in V holds
[v1,(the_Edges_of G2)] DJoins v1,v,G1
let v be object ; :: thesis: for V being set
for G1 being addAdjVertexFromAll of G2,v,V
for v1 being object st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & v1 in V holds
[v1,(the_Edges_of G2)] DJoins v1,v,G1
let V be set ; :: thesis: for G1 being addAdjVertexFromAll of G2,v,V
for v1 being object st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & v1 in V holds
[v1,(the_Edges_of G2)] DJoins v1,v,G1
let G1 be addAdjVertexFromAll of G2,v,V; :: thesis: for v1 being object st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & v1 in V holds
[v1,(the_Edges_of G2)] DJoins v1,v,G1
let v1 be object ; :: thesis: ( V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & v1 in V implies [v1,(the_Edges_of G2)] DJoins v1,v,G1 )
assume A1: ( V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & v1 in V ) ; :: thesis: [v1,(the_Edges_of G2)] DJoins v1,v,G1
then A2: ( the_Edges_of G1 = (the_Edges_of G2) \/ (V --> (the_Edges_of G2)) & the_Source_of G1 = (the_Source_of G2) +* (pr1 (V,{(the_Edges_of G2)})) & the_Target_of G1 = (the_Target_of G2) +* ((V --> (the_Edges_of G2)) --> v) ) by Def3;
set e = [v1,(the_Edges_of G2)];
A3: the_Edges_of G2 in {(the_Edges_of G2)} by TARSKI:def 1;
then A4: [v1,(the_Edges_of G2)] in [:V,{(the_Edges_of G2)}:] by A1, ZFMISC_1:def 2;
then A5: [v1,(the_Edges_of G2)] in V --> (the_Edges_of G2) by FUNCOP_1:def 2;
then A6: [v1,(the_Edges_of G2)] in dom ((V --> (the_Edges_of G2)) --> v) ;
A7: [v1,(the_Edges_of G2)] in dom (pr1 (V,{(the_Edges_of G2)})) by A4, FUNCT_3:def 4;
A8: [v1,(the_Edges_of G2)] in the_Edges_of G1 by A2, A5, XBOOLE_0:def 3;
A9: (the_Target_of G1) . [v1,(the_Edges_of G2)] = ((V --> (the_Edges_of G2)) --> v) . [v1,(the_Edges_of G2)] by A2, A6, FUNCT_4:13
.= v by A5, FUNCOP_1:7 ;
(the_Source_of G1) . [v1,(the_Edges_of G2)] = (pr1 (V,{(the_Edges_of G2)})) . [v1,(the_Edges_of G2)] by A2, A7, FUNCT_4:13
.= (pr1 (V,{(the_Edges_of G2)})) . (v1,(the_Edges_of G2)) by BINOP_1:def 1
.= v1 by A1, A3, FUNCT_3:def 4 ;
hence [v1,(the_Edges_of G2)] DJoins v1,v,G1 by A8, A9, GLIB_000:def 14; :: thesis: verum