let G2 be _Graph; :: thesis:
let v, e, w be object ; :: thesis:
let G1 be addAdjVertex of G2,v,e,w; :: thesis:
let f1 be VColoring of G1; :: thesis:
let f2 be VColoring of G2; :: thesis:
let x be object ; :: thesis:
assume that
A1: ( not w in the_Vertices_of G2 & f1 = f2 +* (w .--> x) ) and
A2: ( x <> f2 . v & f2 is proper ) ; :: thesis:
set G3 = the reverseEdgeDirections of G1,{e};

per cases ;

suppose not e in the_Edges_of G2 ; :: thesis:

then A3: the reverseEdgeDirections of G1,{e} is addAdjVertex of G2,w,e,v by GLIBPRE1:66;
the_Vertices_of G1 = the_Vertices_of the reverseEdgeDirections of G1,{e} by GLIB_007:4;
then reconsider f3 = f1 as VColoring of the reverseEdgeDirections of G1,{e} ;
f3 is proper by A1, A2, A3, Th23;
hence f1 is proper by Th18; :: thesis:

end;

suppose e in the_Edges_of G2 ; :: thesis:

then G1 == G2 by GLIB_006:def 12;
then the_Vertices_of G2 = the_Vertices_of G1 by GLIB_000:def 34
.= dom f1 by PARTFUN1:def 2
.= (dom f2) \/ (dom (w .--> x)) by A1, FUNCT_4:def 1
.= (dom f2) \/ (dom {[w,x]}) by FUNCT_4:82
.= (dom f2) \/ {w} by RELAT_1:9
.= (the_Vertices_of G2) \/ {w} by PARTFUN1:def 2 ;
hence f1 is proper by A1, ZFMISC_1:39; :: thesis:

end;

end;