theorem :: GLIB_016:62

for G2 being _Graph
for V being set
for G1 being addVertices of G2,V holds
( G1 .degreeMap() = (G2 .degreeMap()) +* ((V \ (the_Vertices_of G2)) --> 0) & G1 .inDegreeMap() = (G2 .inDegreeMap()) +* ((V \ (the_Vertices_of G2)) --> 0) & G1 .outDegreeMap() = (G2 .outDegreeMap()) +* ((V \ (the_Vertices_of G2)) --> 0) )