let G be _Graph; :: thesis: for v being Vertex of G holds (G .degreeMap()) . v = ((G .inDegreeMap()) . v) +` ((G .outDegreeMap()) . v)
let v be Vertex of G; :: thesis: (G .degreeMap()) . v = ((G .inDegreeMap()) . v) +` ((G .outDegreeMap()) . v)
thus (G .degreeMap()) . v = v .degree() by Def11
.= ((G .inDegreeMap()) . v) +` (v .outDegree()) by Def12
.= ((G .inDegreeMap()) . v) +` ((G .outDegreeMap()) . v) by Def13 ; :: thesis: verum