let G be _Graph; :: thesis: for C being Component of G holds
( C .degreeMap() = (G .degreeMap()) | (the_Vertices_of C) & C .inDegreeMap() = (G .inDegreeMap()) | (the_Vertices_of C) & C .outDegreeMap() = (G .outDegreeMap()) | (the_Vertices_of C) )
let C be Component of G; :: thesis: ( C .degreeMap() = (G .degreeMap()) | (the_Vertices_of C) & C .inDegreeMap() = (G .inDegreeMap()) | (the_Vertices_of C) & C .outDegreeMap() = (G .outDegreeMap()) | (the_Vertices_of C) )
A1: the_Vertices_of C c= the_Vertices_of G ;
A2: dom (C .degreeMap()) = the_Vertices_of C by PARTFUN1:def 2
.= (the_Vertices_of C) /\ (the_Vertices_of G) by XBOOLE_1:28
.= (dom (G .degreeMap())) /\ (the_Vertices_of C) by PARTFUN1:def 2
.= dom ((G .degreeMap()) | (the_Vertices_of C)) by RELAT_1:61 ;

now :: thesis: for x being object st x in dom (C .degreeMap()) holds
(C .degreeMap()) . x = ((G .degreeMap()) | (the_Vertices_of C)) . x

let x be object ; :: thesis: ( x in dom (C .degreeMap()) implies (C .degreeMap()) . x = ((G .degreeMap()) | (the_Vertices_of C)) . x )
assume A3: x in dom (C .degreeMap()) ; :: thesis: (C .degreeMap()) . x = ((G .degreeMap()) | (the_Vertices_of C)) . x
then reconsider v2 = x as Vertex of C ;
reconsider v1 = v2 as Vertex of G by A1, TARSKI:def 3;
thus (C .degreeMap()) . x = v2 .degree() by Def11
.= v1 .degree() by GLIBPRE0:44
.= (G .degreeMap()) . x by Def11
.= ((G .degreeMap()) | (the_Vertices_of C)) . x by A3, FUNCT_1:49 ; :: thesis: verum

end;

hence C .degreeMap() = (G .degreeMap()) | (the_Vertices_of C) by A2, FUNCT_1:2; :: thesis: ( C .inDegreeMap() = (G .inDegreeMap()) | (the_Vertices_of C) & C .outDegreeMap() = (G .outDegreeMap()) | (the_Vertices_of C) )
A4: dom (C .inDegreeMap()) = the_Vertices_of C by PARTFUN1:def 2
.= (the_Vertices_of C) /\ (the_Vertices_of G) by XBOOLE_1:28
.= (dom (G .inDegreeMap())) /\ (the_Vertices_of C) by PARTFUN1:def 2
.= dom ((G .inDegreeMap()) | (the_Vertices_of C)) by RELAT_1:61 ;

now :: thesis: for x being object st x in dom (C .inDegreeMap()) holds
(C .inDegreeMap()) . x = ((G .inDegreeMap()) | (the_Vertices_of C)) . x

let x be object ; :: thesis: ( x in dom (C .inDegreeMap()) implies (C .inDegreeMap()) . x = ((G .inDegreeMap()) | (the_Vertices_of C)) . x )
assume A5: x in dom (C .inDegreeMap()) ; :: thesis: (C .inDegreeMap()) . x = ((G .inDegreeMap()) | (the_Vertices_of C)) . x
then reconsider v2 = x as Vertex of C ;
reconsider v1 = v2 as Vertex of G by A1, TARSKI:def 3;
thus (C .inDegreeMap()) . x = v2 .inDegree() by Def12
.= v1 .inDegree() by GLIBPRE0:44
.= (G .inDegreeMap()) . x by Def12
.= ((G .inDegreeMap()) | (the_Vertices_of C)) . x by A5, FUNCT_1:49 ; :: thesis: verum

end;

hence C .inDegreeMap() = (G .inDegreeMap()) | (the_Vertices_of C) by A4, FUNCT_1:2; :: thesis: C .outDegreeMap() = (G .outDegreeMap()) | (the_Vertices_of C)
A6: dom (C .outDegreeMap()) = the_Vertices_of C by PARTFUN1:def 2
.= (the_Vertices_of C) /\ (the_Vertices_of G) by XBOOLE_1:28
.= (dom (G .outDegreeMap())) /\ (the_Vertices_of C) by PARTFUN1:def 2
.= dom ((G .outDegreeMap()) | (the_Vertices_of C)) by RELAT_1:61 ;

now :: thesis: for x being object st x in dom (C .outDegreeMap()) holds
(C .outDegreeMap()) . x = ((G .outDegreeMap()) | (the_Vertices_of C)) . x

let x be object ; :: thesis: ( x in dom (C .outDegreeMap()) implies (C .outDegreeMap()) . x = ((G .outDegreeMap()) | (the_Vertices_of C)) . x )
assume A7: x in dom (C .outDegreeMap()) ; :: thesis: (C .outDegreeMap()) . x = ((G .outDegreeMap()) | (the_Vertices_of C)) . x
then reconsider v2 = x as Vertex of C ;
reconsider v1 = v2 as Vertex of G by A1, TARSKI:def 3;
thus (C .outDegreeMap()) . x = v2 .outDegree() by Def13
.= v1 .outDegree() by GLIBPRE0:44
.= (G .outDegreeMap()) . x by Def13
.= ((G .outDegreeMap()) | (the_Vertices_of C)) . x by A7, FUNCT_1:49 ; :: thesis: verum

end;

hence C .outDegreeMap() = (G .outDegreeMap()) | (the_Vertices_of C) by A6, FUNCT_1:2; :: thesis: verum