let G2 be _Graph; :: thesis: for v being object
for V being set
for G1 being addAdjVertexToAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 holds
G1 .edgesOutOf {v} = V --> (the_Edges_of G2)
let v be object ; :: thesis: for V being set
for G1 being addAdjVertexToAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 holds
G1 .edgesOutOf {v} = V --> (the_Edges_of G2)
let V be set ; :: thesis: for G1 being addAdjVertexToAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 holds
G1 .edgesOutOf {v} = V --> (the_Edges_of G2)
let G1 be addAdjVertexToAll of G2,v,V; :: thesis: ( V c= the_Vertices_of G2 & not v in the_Vertices_of G2 implies G1 .edgesOutOf {v} = V --> (the_Edges_of G2) )
assume A1: ( V c= the_Vertices_of G2 & not v in the_Vertices_of G2 ) ; :: thesis: G1 .edgesOutOf {v} = V --> (the_Edges_of G2)
then A2: ( the_Edges_of G1 = (the_Edges_of G2) \/ (V --> (the_Edges_of G2)) & the_Source_of G1 = (the_Source_of G2) +* ((V --> (the_Edges_of G2)) --> v) ) by Def2;
for e being object holds
( e in G1 .edgesOutOf {v} iff e in V --> (the_Edges_of G2) )

proof

let e be object ; :: thesis: ( e in G1 .edgesOutOf {v} iff e in V --> (the_Edges_of G2) )
reconsider e1 = e as set by TARSKI:1;

hereby :: thesis: ( e in V --> (the_Edges_of G2) implies e in G1 .edgesOutOf {v} )

assume e in G1 .edgesOutOf {v} ; :: thesis: e in V --> (the_Edges_of G2)
then A3: ( e1 in the_Edges_of G1 & (the_Source_of G1) . e1 in {v} ) by GLIB_000:def 27;
not e in the_Edges_of G2

proof

assume A4: e in the_Edges_of G2 ; :: thesis: contradiction
then (the_Source_of G2) . e1 = (the_Source_of G1) . e1 by GLIB_006:def 9
.= v by A3, TARSKI:def 1 ;
hence contradiction by A1, A4, FUNCT_2:5; :: thesis: verum

end;

hence e in V --> (the_Edges_of G2) by A2, A3, XBOOLE_0:def 3; :: thesis: verum

end;

assume A5: e in V --> (the_Edges_of G2) ; :: thesis: e in G1 .edgesOutOf {v}
then e in dom ((V --> (the_Edges_of G2)) --> v) ;
then (the_Source_of G1) . e = ((V --> (the_Edges_of G2)) --> v) . e by A2, FUNCT_4:13
.= v by A5, FUNCOP_1:7 ;
then A6: (the_Source_of G1) . e in {v} by TARSKI:def 1;
e in the_Edges_of G1 by A5, A2, XBOOLE_0:def 3;
hence e in G1 .edgesOutOf {v} by A6, GLIB_000:def 27; :: thesis: verum

end;

hence G1 .edgesOutOf {v} = V --> (the_Edges_of G2) by TARSKI:2; :: thesis: verum