let G be _finite _Graph; :: thesis: for v being Denumeration of (the_Vertices_of G) holds 2 * (G .size()) = Sum ((G .degreeMap()) * v)
let v be Denumeration of (the_Vertices_of G); :: thesis: 2 * (G .size()) = Sum ((G .degreeMap()) * v)
thus 2 * (G .size()) = (G .size()) + (G .size())
.= (Sum ((G .inDegreeMap()) * v)) + (G .size()) by Th65
.= (Sum ((G .inDegreeMap()) * v)) + (Sum ((G .outDegreeMap()) * v)) by Th65
.= Sum (((G .inDegreeMap()) * v) + ((G .outDegreeMap()) * v)) by RVSUM_4:49
.= Sum ((G .degreeMap()) * v) by Th64 ; :: thesis: verum