let G2 be _Graph; :: thesis:
let v be Vertex of G2; :: thesis:
let e, w be object ; :: thesis:
let G1 be addEdge 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 A1: ( f1 = f2 +* (v .--> x) & v <> w & not x in rng f2 & f2 is proper ) ; :: thesis:

per cases ;

suppose A2: ( not e in the_Edges_of G2 & v in the_Vertices_of G2 & w in the_Vertices_of G2 ) ; :: thesis:

set h = v .--> x;

now :: thesis:

let e9, v9, w9 be object ; :: thesis:
assume A3: e9 Joins v9,w9,G1 ; :: thesis:

per cases ;

suppose e9 in the_Edges_of G2 ; :: thesis:

then A4: e9 Joins v9,w9,G2 by A3, GLIB_006:72;
( v9 in the_Vertices_of G2 & w9 in the_Vertices_of G2 ) by A4, GLIB_000:13;
then ( v9 in dom f2 & w9 in dom f2 ) by PARTFUN1:def 2;
then A5: ( f2 . v9 in rng f2 & f2 . w9 in rng f2 ) by FUNCT_1:3;

per cases ;

suppose ( v9 <> v & w9 <> v ) ; :: thesis:

then ( f1 . v9 = f2 . v9 & f1 . w9 = f2 . w9 ) by A1, FUNCT_4:83;
hence f1 . v9 <> f1 . w9 by A1, A4, Th10; :: thesis:

end;

suppose ( v9 = v & w9 <> v ) ; :: thesis:

then ( f1 . v9 = x & f1 . w9 = f2 . w9 ) by A1, FUNCT_4:83, FUNCT_4:113;
hence f1 . v9 <> f1 . w9 by A1, A5; :: thesis:

end;

suppose ( v9 <> v & w9 = v ) ; :: thesis:

then ( f1 . v9 = f2 . v9 & f1 . w9 = x ) by A1, FUNCT_4:83, FUNCT_4:113;
hence f1 . v9 <> f1 . w9 by A1, A5; :: thesis:

end;

suppose ( v9 = v & w9 = v ) ; :: thesis:

then not G2 is loopless by A4, GLIB_000:18;
hence f1 . v9 <> f1 . w9 by A1; :: thesis:

end;

end;

end;

suppose A6: not e9 in the_Edges_of G2 ; :: thesis:

w in dom f2 by A2, PARTFUN1:def 2;
then A7: f2 . w in rng f2 by FUNCT_1:3;

per cases by A2, A3, A6, GLIB_006:107;

suppose A8: ( v9 = w & w9 = v ) ; :: thesis:

then ( f1 . v9 = f2 . v9 & f1 . w9 = x ) by A1, FUNCT_4:83, FUNCT_4:113;
hence f1 . v9 <> f1 . w9 by A1, A8, A7; :: thesis:

end;

suppose A9: ( v9 = v & w9 = w ) ; :: thesis:

then ( f1 . v9 = x & f1 . w9 = f2 . w9 ) by A1, FUNCT_4:83, FUNCT_4:113;
hence f1 . v9 <> f1 . w9 by A1, A9, A7; :: thesis:

end;

end;

end;

end;

end;

hence f1 is proper by Th10; :: thesis:

end;

suppose ( e in the_Edges_of G2 or not v in the_Vertices_of G2 or not w in the_Vertices_of G2 ) ; :: thesis:

then G1 == G2 by GLIB_006:def 11;
hence f1 is proper by A1, Th17; :: thesis:

end;

end;