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

proof

let e be object ; :: thesis: ( e in G1 .edgesInto {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 .edgesInto {v} )

assume e in G1 .edgesInto {v} ; :: thesis: e in V --> (the_Edges_of G2)
then A3: ( e1 in the_Edges_of G1 & (the_Target_of G1) . e1 in {v} ) by GLIB_000:def 26;
then A4: (the_Target_of G1) . e = v by TARSKI:def 1;
not e in the_Edges_of G2

proof

assume A5: e in the_Edges_of G2 ; :: thesis: contradiction
then (the_Target_of G2) . e1 = v by A4, GLIB_006:def 9;
hence contradiction by A1, A5, 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 A6: e in V --> (the_Edges_of G2) ; :: thesis: e in G1 .edgesInto {v}
then e in dom ((V --> (the_Edges_of G2)) --> v) ;
then (the_Target_of G1) . e = ((V --> (the_Edges_of G2)) --> v) . e by A2, FUNCT_4:13
.= v by A6, FUNCOP_1:7 ;
then A7: (the_Target_of G1) . e in {v} by TARSKI:def 1;
e in the_Edges_of G1 by A6, A2, XBOOLE_0:def 3;
hence e in G1 .edgesInto {v} by A7, GLIB_000:def 26; :: thesis: verum

end;

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