let G2 be _Graph; :: thesis: for v, x being object
for V being Subset of (the_Vertices_of G2)
for G1 being addAdjVertexAll of G2,v,V
for f2 being VColoring of G2 st not v in the_Vertices_of G2 holds
f2 +* (v .--> x) is VColoring of G1
let v, x be object ; :: thesis: for V being Subset of (the_Vertices_of G2)
for G1 being addAdjVertexAll of G2,v,V
for f2 being VColoring of G2 st not v in the_Vertices_of G2 holds
f2 +* (v .--> x) is VColoring of G1
let V be Subset of (the_Vertices_of G2); :: thesis: for G1 being addAdjVertexAll of G2,v,V
for f2 being VColoring of G2 st not v in the_Vertices_of G2 holds
f2 +* (v .--> x) is VColoring of G1
let G1 be addAdjVertexAll of G2,v,V; :: thesis: for f2 being VColoring of G2 st not v in the_Vertices_of G2 holds
f2 +* (v .--> x) is VColoring of G1
let f2 be VColoring of G2; :: thesis: ( not v in the_Vertices_of G2 implies f2 +* (v .--> x) is VColoring of G1 )
set f1 = f2 +* (v .--> x);
assume not v in the_Vertices_of G2 ; :: thesis: f2 +* (v .--> x) is VColoring of G1
then A1: the_Vertices_of G1 = (the_Vertices_of G2) \/ {v} by GLIB_007:def 4;
dom (f2 +* (v .--> x)) = (dom f2) \/ (dom (v .--> x)) by FUNCT_4:def 1
.= (dom f2) \/ (dom {[v,x]}) by FUNCT_4:82
.= (dom f2) \/ {v} by RELAT_1:9
.= the_Vertices_of G1 by A1, PARTFUN1:def 2 ;
hence f2 +* (v .--> x) is VColoring of G1 by RELAT_1:def 18, PARTFUN1:def 2; :: thesis: verum