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