let G2 be _Graph; :: thesis: for v, e, x being object
for w being Vertex of G2
for G1 being addAdjVertex of G2,v,e,w
for f being VColoring of G2 st not e in the_Edges_of G2 & not v in the_Vertices_of G2 holds
f +* (v .--> x) is VColoring of G1
let v, e, x be object ; :: thesis: for w being Vertex of G2
for G1 being addAdjVertex of G2,v,e,w
for f being VColoring of G2 st not e in the_Edges_of G2 & not v in the_Vertices_of G2 holds
f +* (v .--> x) is VColoring of G1
let w be Vertex of G2; :: thesis: for G1 being addAdjVertex of G2,v,e,w
for f being VColoring of G2 st not e in the_Edges_of G2 & not v in the_Vertices_of G2 holds
f +* (v .--> x) is VColoring of G1
let G1 be addAdjVertex of G2,v,e,w; :: thesis: for f being VColoring of G2 st not e in the_Edges_of G2 & not v in the_Vertices_of G2 holds
f +* (v .--> x) is VColoring of G1
let f be VColoring of G2; :: thesis: ( not e in the_Edges_of G2 & not v in the_Vertices_of G2 implies f +* (v .--> x) is VColoring of G1 )
assume ( not e in the_Edges_of G2 & not v in the_Vertices_of G2 ) ; :: thesis: f +* (v .--> x) is VColoring of G1
then the_Vertices_of G1 = (the_Vertices_of G2) \/ {v} by GLIB_006:def 12
.= (dom f) \/ {v} by PARTFUN1:def 2
.= (dom f) \/ (dom {[v,x]}) by RELAT_1:9
.= (dom f) \/ (dom (v .--> x)) by FUNCT_4:82
.= dom (f +* (v .--> x)) by FUNCT_4:def 1 ;
hence f +* (v .--> x) is VColoring of G1 by RELAT_1:def 18, PARTFUN1:def 2; :: thesis: verum