theorem :: GLIB_016:63

for G being _Graph
for C being Component of G holds
( C .degreeMap() = (G .degreeMap()) | (the_Vertices_of C) & C .inDegreeMap() = (G .inDegreeMap()) | (the_Vertices_of C) & C .outDegreeMap() = (G .outDegreeMap()) | (the_Vertices_of C) )