theorem Th65: :: GLIB_016:65
for G being _finite _Graph
for v being Denumeration of (the_Vertices_of G) holds
( G .size() = Sum ((G .inDegreeMap()) * v) & G .size() = Sum ((G .outDegreeMap()) * v) )