let G1, G2 be _Graph; :: thesis:
let f1 be VColoring of G1; :: thesis:
let f2 be VColoring of G2; :: thesis:
let v be Vertex of G1; :: thesis:
let x be object ; :: thesis:
assume A1: ( G1 == G2 & f2 = f1 +* (v .--> x) & not x in rng f1 & f1 is proper ) ; :: thesis:

now :: thesis:

let e, u, w be object ; :: thesis:
assume e Joins u,w,G2 ; :: thesis:
then A2: e Joins u,w,G1 by A1, GLIB_000:88;
( u in the_Vertices_of G1 & w in the_Vertices_of G1 ) by A2, GLIB_000:13;
then ( u in dom f1 & w in dom f1 ) by PARTFUN1:def 2;
then A3: ( f1 . u in rng f1 & f1 . w in rng f1 ) by FUNCT_1:3;

per cases ;

suppose ( u <> v & w <> v ) ; :: thesis:

then ( f2 . u = f1 . u & f2 . w = f1 . w ) by A1, FUNCT_4:83;
hence f2 . u <> f2 . w by A1, A2, Th10; :: thesis:

end;

suppose ( u = v & w <> v ) ; :: thesis:

then ( f2 . u = x & f2 . w = f1 . w ) by A1, FUNCT_4:83, FUNCT_4:113;
hence f2 . u <> f2 . w by A1, A3; :: thesis:

end;

suppose ( u <> v & w = v ) ; :: thesis:

then ( f2 . u = f1 . u & f2 . w = x ) by A1, FUNCT_4:83, FUNCT_4:113;
hence f2 . u <> f2 . w by A1, A3; :: thesis:

end;

suppose ( u = v & w = v ) ; :: thesis:

then not G1 is loopless by A2, GLIB_000:18;
hence f2 . u <> f2 . w by A1; :: thesis:

end;

end;

end;

hence f2 is proper by Th10; :: thesis: