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