let G2 be _Graph; :: thesis: for e being object
for v, w being Vertex of G2
for G1 being addEdge of G2,v,e,w
for g being EColoring of G2
for x being object st not e in the_Edges_of G2 holds
g +* (e .--> x) is EColoring of G1
let e be object ; :: thesis: for v, w being Vertex of G2
for G1 being addEdge of G2,v,e,w
for g being EColoring of G2
for x being object st not e in the_Edges_of G2 holds
g +* (e .--> x) is EColoring of G1
let v, w be Vertex of G2; :: thesis: for G1 being addEdge of G2,v,e,w
for g being EColoring of G2
for x being object st not e in the_Edges_of G2 holds
g +* (e .--> x) is EColoring of G1
let G1 be addEdge of G2,v,e,w; :: thesis: for g being EColoring of G2
for x being object st not e in the_Edges_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 holds
g +* (e .--> x) is EColoring of G1
let x be object ; :: thesis: ( not e in the_Edges_of G2 implies g +* (e .--> x) is EColoring of G1 )
assume A1: not e in the_Edges_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 11 ;
hence g +* (e .--> x) is EColoring of G1 by RELAT_1:def 18, PARTFUN1:def 2; :: thesis: verum