theorem Th64: :: GLIB_016:64

for G being _finite _Graph
for v being Denumeration of (the_Vertices_of G) holds (G .degreeMap()) * v = ((G .inDegreeMap()) * v) + ((G .outDegreeMap()) * v)