let G be _finite _Graph; :: thesis: for v being Denumeration of (the_Vertices_of G) holds (G .degreeMap()) * v = ((G .inDegreeMap()) * v) + ((G .outDegreeMap()) * v)
let v be Denumeration of (the_Vertices_of G); :: thesis: (G .degreeMap()) * v = ((G .inDegreeMap()) * v) + ((G .outDegreeMap()) * v)
dom (G .degreeMap()) = the_Vertices_of G by PARTFUN1:def 2
.= rng v by FUNCT_2:def 3 ;
then A1: dom ((G .degreeMap()) * v) = dom v by RELAT_1:27;
dom (G .inDegreeMap()) = the_Vertices_of G by PARTFUN1:def 2
.= rng v by FUNCT_2:def 3 ;
then A2: dom ((G .inDegreeMap()) * v) = dom v by RELAT_1:27;
dom (G .outDegreeMap()) = the_Vertices_of G by PARTFUN1:def 2
.= rng v by FUNCT_2:def 3 ;
then dom ((G .outDegreeMap()) * v) = dom v by RELAT_1:27;
then A3: dom ((G .degreeMap()) * v) = (dom ((G .inDegreeMap()) * v)) /\ (dom ((G .outDegreeMap()) * v)) by A1, A2;

now :: thesis: for c being object st c in dom ((G .degreeMap()) * v) holds
((G .degreeMap()) * v) . c = (((G .inDegreeMap()) * v) . c) + (((G .outDegreeMap()) * v) . c)

let c be object ; :: thesis: ( c in dom ((G .degreeMap()) * v) implies ((G .degreeMap()) * v) . c = (((G .inDegreeMap()) * v) . c) + (((G .outDegreeMap()) * v) . c) )
assume c in dom ((G .degreeMap()) * v) ; :: thesis: ((G .degreeMap()) * v) . c = (((G .inDegreeMap()) * v) . c) + (((G .outDegreeMap()) * v) . c)
then A4: c in dom v by A1;
then v . c in rng v by FUNCT_1:3;
then reconsider w = v . c as Vertex of G ;
thus ((G .degreeMap()) * v) . c = (G .degreeMap()) . w by A4, FUNCT_1:13
.= ((G .inDegreeMap()) . w) +` ((G .outDegreeMap()) . w) by Th60
.= (((G .inDegreeMap()) * v) . c) + ((G .outDegreeMap()) . w) by A4, FUNCT_1:13
.= (((G .inDegreeMap()) * v) . c) + (((G .outDegreeMap()) * v) . c) by A4, FUNCT_1:13 ; :: thesis: verum

end;

hence (G .degreeMap()) * v = ((G .inDegreeMap()) * v) + ((G .outDegreeMap()) * v) by A3, VALUED_1:def 1; :: thesis: verum