let G2 be _Graph; :: thesis: for v, x being object
for G1 being addVertex of G2,v
for t being TColoring of G2 holds [((t _V) +* (v .--> x)),(t _E)] is TColoring of G1
let v, x be object ; :: thesis: for G1 being addVertex of G2,v
for t being TColoring of G2 holds [((t _V) +* (v .--> x)),(t _E)] is TColoring of G1
let G1 be addVertex of G2,v; :: thesis: for t being TColoring of G2 holds [((t _V) +* (v .--> x)),(t _E)] is TColoring of G1
let t be TColoring of G2; :: thesis: [((t _V) +* (v .--> x)),(t _E)] is TColoring of G1
A1: dom (v .--> x) = dom {[v,x]} by FUNCT_4:82
.= {v} by RELAT_1:9 ;
dom ((t _V) +* (v .--> x)) = (dom (t _V)) \/ (dom (v .--> x)) by FUNCT_4:def 1
.= (the_Vertices_of G2) \/ {v} by A1, PARTFUN1:def 2
.= the_Vertices_of G1 by GLIB_006:def 10 ;
then A2: (t _V) +* (v .--> x) is VColoring of G1 by RELAT_1:def 18, PARTFUN1:def 2;
the_Edges_of G1 = the_Edges_of G2 by GLIB_006:def 10;
hence [((t _V) +* (v .--> x)),(t _E)] is TColoring of G1 by A2, Def9; :: thesis: verum