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