let G2 be _Graph; :: thesis: for V being Subset of (the_Vertices_of G2)
for G1 being addLoops of G2,V
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 & v1 in V holds
( v1 .inDegree() = (v2 .inDegree()) +` 1 & v1 .outDegree() = (v2 .outDegree()) +` 1 & v1 .degree() = (v2 .degree()) +` 2 )
let V be Subset of (the_Vertices_of G2); :: thesis: for G1 being addLoops of G2,V
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 & v1 in V holds
( v1 .inDegree() = (v2 .inDegree()) +` 1 & v1 .outDegree() = (v2 .outDegree()) +` 1 & v1 .degree() = (v2 .degree()) +` 2 )
let G1 be addLoops of G2,V; :: thesis: for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 & v1 in V holds
( v1 .inDegree() = (v2 .inDegree()) +` 1 & v1 .outDegree() = (v2 .outDegree()) +` 1 & v1 .degree() = (v2 .degree()) +` 2 )
let v1 be Vertex of G1; :: thesis: for v2 being Vertex of G2 st v1 = v2 & v1 in V holds
( v1 .inDegree() = (v2 .inDegree()) +` 1 & v1 .outDegree() = (v2 .outDegree()) +` 1 & v1 .degree() = (v2 .degree()) +` 2 )
let v2 be Vertex of G2; :: thesis: ( v1 = v2 & v1 in V implies ( v1 .inDegree() = (v2 .inDegree()) +` 1 & v1 .outDegree() = (v2 .outDegree()) +` 1 & v1 .degree() = (v2 .degree()) +` 2 ) )
assume ( v1 = v2 & v1 in V ) ; :: thesis: ( v1 .inDegree() = (v2 .inDegree()) +` 1 & v1 .outDegree() = (v2 .outDegree()) +` 1 & v1 .degree() = (v2 .degree()) +` 2 )
then consider e being object such that
A1: ( e DJoins v1,v1,G1 & not e in the_Edges_of G2 ) and
A2: v1 .edgesIn() = (v2 .edgesIn()) \/ {e} and
A3: v1 .edgesOut() = (v2 .edgesOut()) \/ {e} and
v1 .edgesInOut() = (v2 .edgesInOut()) \/ {e} by Th42;
not e in v2 .edgesIn() by A1;
hence A4: v1 .inDegree() = (v2 .inDegree()) +` (card {e}) by A2, CARD_2:35, ZFMISC_1:50
.= (v2 .inDegree()) +` 1 by CARD_1:30 ;
:: thesis: ( v1 .outDegree() = (v2 .outDegree()) +` 1 & v1 .degree() = (v2 .degree()) +` 2 )
not e in v2 .edgesOut() by A1;
hence v1 .outDegree() = (v2 .outDegree()) +` (card {e}) by A3, CARD_2:35, ZFMISC_1:50
.= (v2 .outDegree()) +` 1 by CARD_1:30 ;
:: thesis: v1 .degree() = (v2 .degree()) +` 2
hence v1 .degree() = (v2 .inDegree()) +` (1 +` ((v2 .outDegree()) +` 1)) by A4, CARD_2:19
.= (v2 .inDegree()) +` ((v2 .outDegree()) +` (1 +` 1)) by CARD_2:19
.= (v2 .degree()) +` 2 by CARD_2:19 ;
:: thesis: verum