let G2 be _Graph; :: thesis: for V being set
for G1 being addVertices of G2,V holds
( G1 .degreeMap() = (G2 .degreeMap()) +* ((V \ (the_Vertices_of G2)) --> 0) & G1 .inDegreeMap() = (G2 .inDegreeMap()) +* ((V \ (the_Vertices_of G2)) --> 0) & G1 .outDegreeMap() = (G2 .outDegreeMap()) +* ((V \ (the_Vertices_of G2)) --> 0) )
let V be set ; :: thesis: for G1 being addVertices of G2,V holds
( G1 .degreeMap() = (G2 .degreeMap()) +* ((V \ (the_Vertices_of G2)) --> 0) & G1 .inDegreeMap() = (G2 .inDegreeMap()) +* ((V \ (the_Vertices_of G2)) --> 0) & G1 .outDegreeMap() = (G2 .outDegreeMap()) +* ((V \ (the_Vertices_of G2)) --> 0) )
let G1 be addVertices of G2,V; :: thesis: ( G1 .degreeMap() = (G2 .degreeMap()) +* ((V \ (the_Vertices_of G2)) --> 0) & G1 .inDegreeMap() = (G2 .inDegreeMap()) +* ((V \ (the_Vertices_of G2)) --> 0) & G1 .outDegreeMap() = (G2 .outDegreeMap()) +* ((V \ (the_Vertices_of G2)) --> 0) )
set f = (V \ (the_Vertices_of G2)) --> 0;
A1: ( dom (G2 .degreeMap()) = the_Vertices_of G2 & dom (G2 .inDegreeMap()) = the_Vertices_of G2 & dom (G2 .outDegreeMap()) = the_Vertices_of G2 ) by PARTFUN1:def 2;
A2: the_Vertices_of G1 = (the_Vertices_of G2) \/ V by GLIB_006:def 10;
A3: (the_Vertices_of G2) \/ (V \ (the_Vertices_of G2)) = the_Vertices_of G1 by A2, XBOOLE_1:39;
A4: dom (G1 .degreeMap()) = (dom (G2 .degreeMap())) \/ (dom ((V \ (the_Vertices_of G2)) --> 0)) by A1, A3, PARTFUN1:def 2
.= dom ((G2 .degreeMap()) +* ((V \ (the_Vertices_of G2)) --> 0)) by FUNCT_4:def 1 ;

now :: thesis: for x being object st x in dom (G1 .degreeMap()) holds
(G1 .degreeMap()) . x = ((G2 .degreeMap()) +* ((V \ (the_Vertices_of G2)) --> 0)) . x

let x be object ; :: thesis: ( x in dom (G1 .degreeMap()) implies (G1 .degreeMap()) . b₁ = ((G2 .degreeMap()) +* ((V \ (the_Vertices_of G2)) --> 0)) . b₁ )
assume x in dom (G1 .degreeMap()) ; :: thesis: (G1 .degreeMap()) . b₁ = ((G2 .degreeMap()) +* ((V \ (the_Vertices_of G2)) --> 0)) . b₁
then reconsider v = x as Vertex of G1 ;

per cases ( v in dom ((V \ (the_Vertices_of G2)) --> 0) or not v in dom ((V \ (the_Vertices_of G2)) --> 0) ) ;

suppose A5: v in dom ((V \ (the_Vertices_of G2)) --> 0) ; :: thesis: (G1 .degreeMap()) . b₁ = ((G2 .degreeMap()) +* ((V \ (the_Vertices_of G2)) --> 0)) . b₁

then A6: v is isolated by GLIB_006:88;
thus (G1 .degreeMap()) . x = v .degree() by Def11
.= 0 by A6, GLIB_000:157
.= ((V \ (the_Vertices_of G2)) --> 0) . x
.= ((G2 .degreeMap()) +* ((V \ (the_Vertices_of G2)) --> 0)) . x by A5, FUNCT_4:13 ; :: thesis: verum

end;

suppose A7: not v in dom ((V \ (the_Vertices_of G2)) --> 0) ; :: thesis: (G1 .degreeMap()) . b₁ = ((G2 .degreeMap()) +* ((V \ (the_Vertices_of G2)) --> 0)) . b₁

then ( not v in V or v in the_Vertices_of G2 ) by XBOOLE_0:def 5;
then reconsider v9 = v as Vertex of G2 by A2, XBOOLE_0:def 3;
thus (G1 .degreeMap()) . x = v .degree() by Def11
.= v9 .degree() by GLIBPRE0:45
.= (G2 .degreeMap()) . x by Def11
.= ((G2 .degreeMap()) +* ((V \ (the_Vertices_of G2)) --> 0)) . x by A7, FUNCT_4:11 ; :: thesis: verum

end;

end;

end;

hence G1 .degreeMap() = (G2 .degreeMap()) +* ((V \ (the_Vertices_of G2)) --> 0) by A4, FUNCT_1:2; :: thesis: ( G1 .inDegreeMap() = (G2 .inDegreeMap()) +* ((V \ (the_Vertices_of G2)) --> 0) & G1 .outDegreeMap() = (G2 .outDegreeMap()) +* ((V \ (the_Vertices_of G2)) --> 0) )
A8: dom (G1 .inDegreeMap()) = (dom (G2 .inDegreeMap())) \/ (dom ((V \ (the_Vertices_of G2)) --> 0)) by A1, A3, PARTFUN1:def 2
.= dom ((G2 .inDegreeMap()) +* ((V \ (the_Vertices_of G2)) --> 0)) by FUNCT_4:def 1 ;

now :: thesis: for x being object st x in dom (G1 .inDegreeMap()) holds
(G1 .inDegreeMap()) . x = ((G2 .inDegreeMap()) +* ((V \ (the_Vertices_of G2)) --> 0)) . x

let x be object ; :: thesis: ( x in dom (G1 .inDegreeMap()) implies (G1 .inDegreeMap()) . b₁ = ((G2 .inDegreeMap()) +* ((V \ (the_Vertices_of G2)) --> 0)) . b₁ )
assume x in dom (G1 .inDegreeMap()) ; :: thesis: (G1 .inDegreeMap()) . b₁ = ((G2 .inDegreeMap()) +* ((V \ (the_Vertices_of G2)) --> 0)) . b₁
then reconsider v = x as Vertex of G1 ;

per cases ( v in dom ((V \ (the_Vertices_of G2)) --> 0) or not v in dom ((V \ (the_Vertices_of G2)) --> 0) ) ;

suppose A9: v in dom ((V \ (the_Vertices_of G2)) --> 0) ; :: thesis: (G1 .inDegreeMap()) . b₁ = ((G2 .inDegreeMap()) +* ((V \ (the_Vertices_of G2)) --> 0)) . b₁

then A10: v is isolated by GLIB_006:88;
thus (G1 .inDegreeMap()) . x = v .inDegree() by Def12
.= 0 by A10, GLIB_000:156
.= ((V \ (the_Vertices_of G2)) --> 0) . x
.= ((G2 .inDegreeMap()) +* ((V \ (the_Vertices_of G2)) --> 0)) . x by A9, FUNCT_4:13 ; :: thesis: verum

end;

suppose A11: not v in dom ((V \ (the_Vertices_of G2)) --> 0) ; :: thesis: (G1 .inDegreeMap()) . b₁ = ((G2 .inDegreeMap()) +* ((V \ (the_Vertices_of G2)) --> 0)) . b₁

then ( not v in V or v in the_Vertices_of G2 ) by XBOOLE_0:def 5;
then reconsider v9 = v as Vertex of G2 by A2, XBOOLE_0:def 3;
thus (G1 .inDegreeMap()) . x = v .inDegree() by Def12
.= v9 .inDegree() by GLIBPRE0:45
.= (G2 .inDegreeMap()) . x by Def12
.= ((G2 .inDegreeMap()) +* ((V \ (the_Vertices_of G2)) --> 0)) . x by A11, FUNCT_4:11 ; :: thesis: verum

end;

end;

end;

hence G1 .inDegreeMap() = (G2 .inDegreeMap()) +* ((V \ (the_Vertices_of G2)) --> 0) by A8, FUNCT_1:2; :: thesis: G1 .outDegreeMap() = (G2 .outDegreeMap()) +* ((V \ (the_Vertices_of G2)) --> 0)
A12: dom (G1 .outDegreeMap()) = (dom (G2 .outDegreeMap())) \/ (dom ((V \ (the_Vertices_of G2)) --> 0)) by A1, A3, PARTFUN1:def 2
.= dom ((G2 .outDegreeMap()) +* ((V \ (the_Vertices_of G2)) --> 0)) by FUNCT_4:def 1 ;

now :: thesis: for x being object st x in dom (G1 .outDegreeMap()) holds
(G1 .outDegreeMap()) . x = ((G2 .outDegreeMap()) +* ((V \ (the_Vertices_of G2)) --> 0)) . x

let x be object ; :: thesis: ( x in dom (G1 .outDegreeMap()) implies (G1 .outDegreeMap()) . b₁ = ((G2 .outDegreeMap()) +* ((V \ (the_Vertices_of G2)) --> 0)) . b₁ )
assume x in dom (G1 .outDegreeMap()) ; :: thesis: (G1 .outDegreeMap()) . b₁ = ((G2 .outDegreeMap()) +* ((V \ (the_Vertices_of G2)) --> 0)) . b₁
then reconsider v = x as Vertex of G1 ;

per cases ( v in dom ((V \ (the_Vertices_of G2)) --> 0) or not v in dom ((V \ (the_Vertices_of G2)) --> 0) ) ;

suppose A13: v in dom ((V \ (the_Vertices_of G2)) --> 0) ; :: thesis: (G1 .outDegreeMap()) . b₁ = ((G2 .outDegreeMap()) +* ((V \ (the_Vertices_of G2)) --> 0)) . b₁

then A14: v is isolated by GLIB_006:88;
thus (G1 .outDegreeMap()) . x = v .outDegree() by Def13
.= 0 by A14, GLIB_000:156
.= ((V \ (the_Vertices_of G2)) --> 0) . x
.= ((G2 .outDegreeMap()) +* ((V \ (the_Vertices_of G2)) --> 0)) . x by A13, FUNCT_4:13 ; :: thesis: verum

end;

suppose A15: not v in dom ((V \ (the_Vertices_of G2)) --> 0) ; :: thesis: (G1 .outDegreeMap()) . b₁ = ((G2 .outDegreeMap()) +* ((V \ (the_Vertices_of G2)) --> 0)) . b₁

then ( not v in V or v in the_Vertices_of G2 ) by XBOOLE_0:def 5;
then reconsider v9 = v as Vertex of G2 by A2, XBOOLE_0:def 3;
thus (G1 .outDegreeMap()) . x = v .outDegree() by Def13
.= v9 .outDegree() by GLIBPRE0:45
.= (G2 .outDegreeMap()) . x by Def13
.= ((G2 .outDegreeMap()) +* ((V \ (the_Vertices_of G2)) --> 0)) . x by A15, FUNCT_4:11 ; :: thesis: verum

end;

end;

end;

hence G1 .outDegreeMap() = (G2 .outDegreeMap()) +* ((V \ (the_Vertices_of G2)) --> 0) by A12, FUNCT_1:2; :: thesis: verum