let G2 be _Graph; :: thesis:
let V be Subset of (the_Vertices_of G2); :: thesis:
let G1 be addLoops of G2,V; :: thesis:
let v1 be Vertex of G1; :: thesis:
let v2 be Vertex of G2; :: thesis:
assume A1: ( v1 = v2 & not v1 in V ) ; :: thesis:
consider E being set , f being one-to-one Function such that
A2: ( E misses the_Edges_of G2 & the_Edges_of G1 = (the_Edges_of G2) \/ E ) and
A3: ( dom f = E & rng f = V & the_Source_of G1 = (the_Source_of G2) +* f ) and
A4: the_Target_of G1 = (the_Target_of G2) +* f by Def5;
A5: G2 is Subgraph of G1 by GLIB_006:57;
then A6: v2 .edgesIn() c= v1 .edgesIn() by A1, GLIB_000:78;

now :: thesis:

let e be object ; :: thesis:
assume e in v1 .edgesIn() ; :: thesis:
then consider x being set such that
A7: e DJoins x,v1,G1 by GLIB_000:57;
e in the_Edges_of G2

proof

assume A8: not e in the_Edges_of G2 ; :: thesis:
e in the_Edges_of G1 by A7, GLIB_000:def 14;
then A9: e in E by A2, A8, XBOOLE_0:def 3;
v1 = (the_Target_of G1) . e by A7, GLIB_000:def 14
.= f . e by A3, A4, A9, FUNCT_4:13 ;
hence contradiction by A1, A3, A9, FUNCT_1:3; :: thesis:

end;

hence e in v2 .edgesIn() by A1, A7, GLIB_006:71, GLIB_000:57; :: thesis:

end;

then v1 .edgesIn() c= v2 .edgesIn() by TARSKI:def 3;
hence A10: v1 .edgesIn() = v2 .edgesIn() by A6, XBOOLE_0:def 10; :: thesis:
hence v1 .inDegree() = v2 .inDegree() ; :: thesis:
A11: v2 .edgesOut() c= v1 .edgesOut() by A1, A5, GLIB_000:78;

now :: thesis:

let e be object ; :: thesis:
assume e in v1 .edgesOut() ; :: thesis:
then consider x being set such that
A12: e DJoins v1,x,G1 by GLIB_000:59;
e in the_Edges_of G2

proof

assume A13: not e in the_Edges_of G2 ; :: thesis:
e in the_Edges_of G1 by A12, GLIB_000:def 14;
then A14: e in E by A2, A13, XBOOLE_0:def 3;
v1 = (the_Source_of G1) . e by A12, GLIB_000:def 14
.= f . e by A3, A14, FUNCT_4:13 ;
hence contradiction by A1, A3, A14, FUNCT_1:3; :: thesis:

end;

hence e in v2 .edgesOut() by A1, A12, GLIB_006:71, GLIB_000:59; :: thesis:

end;

then v1 .edgesOut() c= v2 .edgesOut() by TARSKI:def 3;
hence A15: v1 .edgesOut() = v2 .edgesOut() by A11, XBOOLE_0:def 10; :: thesis:
hence v1 .outDegree() = v2 .outDegree() ; :: thesis:
thus ( v1 .edgesInOut() = v2 .edgesInOut() & v1 .degree() = v2 .degree() ) by A10, A15; :: thesis: