let G be _Graph; :: thesis:
let C be Component of G; :: thesis:
let v1 be Vertex of G; :: thesis:
let v2 be Vertex of C; :: thesis:
assume A1: v1 = v2 ; :: thesis:
then A2: ( v2 .edgesIn() c= v1 .edgesIn() & v2 .edgesOut() c= v1 .edgesOut() ) by GLIB_000:78;

let e be object ; :: thesis:
assume e in v1 .edgesIn() ; :: thesis:
then consider x being set such that
A3: e DJoins x,v1,G by GLIB_000:57;
set W = G .walkOf (v1,e,x);
A4: e Joins v1,x,G by A3, GLIB_000:16;
then G .walkOf (v1,e,x) is_Walk_from v1,x by GLIB_001:15;
then A5: x in G .reachableFrom v1 by GLIB_002:def 5;
A6: ( e Joins v2,x,G & e DJoins x,v2,G ) by A1, A3, A4;
the_Vertices_of C = G .reachableFrom v1 by A1, GLIB_002:33;
then e in G .edgesBetween (the_Vertices_of C) by A5, A6, GLIB_000:32;
then e in the_Edges_of C by GLIB_002:31;
then ( e DJoins x,v2,C & e is set ) by A6, GLIB_000:73;
hence e in v2 .edgesIn() by GLIB_000:57; :: thesis:

end;

then v1 .edgesIn() c= v2 .edgesIn() by TARSKI:def 3;
hence A7: v1 .edgesIn() = v2 .edgesIn() by A2, XBOOLE_0:def 10; :: thesis:
hence A8: v1 .inDegree() = v2 .inDegree() ; :: thesis:

let e be object ; :: thesis:
assume e in v1 .edgesOut() ; :: thesis:
then consider x being set such that
A9: e DJoins v1,x,G by GLIB_000:59;
set W = G .walkOf (v1,e,x);
A10: e Joins v1,x,G by A9, GLIB_000:16;
then G .walkOf (v1,e,x) is_Walk_from v1,x by GLIB_001:15;
then A11: x in G .reachableFrom v1 by GLIB_002:def 5;
A12: ( e Joins v2,x,G & e DJoins v2,x,G ) by A1, A9, A10;
the_Vertices_of C = G .reachableFrom v1 by A1, GLIB_002:33;
then e in G .edgesBetween (the_Vertices_of C) by A11, A12, GLIB_000:32;
then e in the_Edges_of C by GLIB_002:31;
then ( e DJoins v2,x,C & e is set ) by A12, GLIB_000:73;
hence e in v2 .edgesOut() by GLIB_000:59; :: thesis:

end;

then v1 .edgesOut() c= v2 .edgesOut() by TARSKI:def 3;
hence A13: v1 .edgesOut() = v2 .edgesOut() by A2, XBOOLE_0:def 10; :: thesis:
hence A14: v1 .outDegree() = v2 .outDegree() ; :: thesis:
thus v1 .edgesInOut() = v2 .edgesInOut() by A7, A13; :: thesis:
thus v1 .degree() = v2 .degree() by A8, A14; :: thesis: