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 t being TColoring of G2
for y being object st not e in the_Edges_of G2 holds
[(t _V),((t _E) +* (e .--> y))] is TColoring of G1
let e be object ; :: thesis: for v, w being Vertex of G2
for G1 being addEdge of G2,v,e,w
for t being TColoring of G2
for y being object st not e in the_Edges_of G2 holds
[(t _V),((t _E) +* (e .--> y))] is TColoring of G1
let v, w be Vertex of G2; :: thesis: for G1 being addEdge of G2,v,e,w
for t being TColoring of G2
for y being object st not e in the_Edges_of G2 holds
[(t _V),((t _E) +* (e .--> y))] is TColoring of G1
let G1 be addEdge of G2,v,e,w; :: thesis: for t being TColoring of G2
for y being object st not e in the_Edges_of G2 holds
[(t _V),((t _E) +* (e .--> y))] is TColoring of G1
let t be TColoring of G2; :: thesis: for y being object st not e in the_Edges_of G2 holds
[(t _V),((t _E) +* (e .--> y))] is TColoring of G1
let y be object ; :: thesis: ( not e in the_Edges_of G2 implies [(t _V),((t _E) +* (e .--> y))] is TColoring of G1 )
assume not e in the_Edges_of G2 ; :: thesis: [(t _V),((t _E) +* (e .--> y))] is TColoring of G1
then A1: ( the_Vertices_of G1 = the_Vertices_of G2 & the_Edges_of G1 = (the_Edges_of G2) \/ {e} ) by GLIB_006:def 11;
dom ((t _E) +* (e .--> y)) = (dom (t _E)) \/ (dom (e .--> y)) by FUNCT_4:def 1
.= (the_Edges_of G2) \/ (dom (e .--> y)) by PARTFUN1:def 2
.= (the_Edges_of G2) \/ (dom {[e,y]}) by FUNCT_4:82
.= the_Edges_of G1 by A1, RELAT_1:9 ;
then (t _E) +* (e .--> y) is EColoring of G1 by RELAT_1:def 18, PARTFUN1:def 2;
hence [(t _V),((t _E) +* (e .--> y))] is TColoring of G1 by A1, Def9; :: thesis: verum