let G2 be _Graph; :: thesis: for v being object
for V being Subset of (the_Vertices_of G2)
for G1 being addAdjVertexAll of G2,v,V
for g2 being EColoring of G2
for h being Function st not v in the_Vertices_of G2 & dom h = G1 .edgesBetween (V,{v}) holds
g2 +* h is EColoring of G1
let v be object ; :: thesis: for V being Subset of (the_Vertices_of G2)
for G1 being addAdjVertexAll of G2,v,V
for g2 being EColoring of G2
for h being Function st not v in the_Vertices_of G2 & dom h = G1 .edgesBetween (V,{v}) holds
g2 +* h is EColoring of G1
let V be Subset of (the_Vertices_of G2); :: thesis: for G1 being addAdjVertexAll of G2,v,V
for g2 being EColoring of G2
for h being Function st not v in the_Vertices_of G2 & dom h = G1 .edgesBetween (V,{v}) holds
g2 +* h is EColoring of G1
let G1 be addAdjVertexAll of G2,v,V; :: thesis: for g2 being EColoring of G2
for h being Function st not v in the_Vertices_of G2 & dom h = G1 .edgesBetween (V,{v}) holds
g2 +* h is EColoring of G1
let g2 be EColoring of G2; :: thesis: for h being Function st not v in the_Vertices_of G2 & dom h = G1 .edgesBetween (V,{v}) holds
g2 +* h is EColoring of G1
let h be Function; :: thesis: ( not v in the_Vertices_of G2 & dom h = G1 .edgesBetween (V,{v}) implies g2 +* h is EColoring of G1 )
set E = dom h;
assume A1: ( not v in the_Vertices_of G2 & dom h = G1 .edgesBetween (V,{v}) ) ; :: thesis: g2 +* h is EColoring of G1
dom (g2 +* h) = (dom g2) \/ (dom h) by FUNCT_4:def 1
.= (the_Edges_of G2) \/ (dom h) by PARTFUN1:def 2
.= the_Edges_of G1 by A1, GLIB_007:59 ;
hence g2 +* h is EColoring of G1 by RELAT_1:def 18, PARTFUN1:def 2; :: thesis: verum