let G2 be _Graph; :: thesis: for v, e, w being object
for G1 being addAdjVertex of G2,v,e,w
for f1 being VColoring of G1
for f2 being VColoring of G2
for x being object st not v in the_Vertices_of G2 & f1 = f2 +* (v .--> x) & x <> f2 . w & f2 is proper holds
f1 is proper
let v, e, w be object ; :: thesis: for G1 being addAdjVertex of G2,v,e,w
for f1 being VColoring of G1
for f2 being VColoring of G2
for x being object st not v in the_Vertices_of G2 & f1 = f2 +* (v .--> x) & x <> f2 . w & f2 is proper holds
f1 is proper
let G1 be addAdjVertex of G2,v,e,w; :: thesis: for f1 being VColoring of G1
for f2 being VColoring of G2
for x being object st not v in the_Vertices_of G2 & f1 = f2 +* (v .--> x) & x <> f2 . w & f2 is proper holds
f1 is proper
let f1 be VColoring of G1; :: thesis: for f2 being VColoring of G2
for x being object st not v in the_Vertices_of G2 & f1 = f2 +* (v .--> x) & x <> f2 . w & f2 is proper holds
f1 is proper
let f2 be VColoring of G2; :: thesis: for x being object st not v in the_Vertices_of G2 & f1 = f2 +* (v .--> x) & x <> f2 . w & f2 is proper holds
f1 is proper
let x be object ; :: thesis: ( not v in the_Vertices_of G2 & f1 = f2 +* (v .--> x) & x <> f2 . w & f2 is proper implies f1 is proper )
assume that
A1: ( not v in the_Vertices_of G2 & f1 = f2 +* (v .--> x) ) and
A2: ( x <> f2 . w & f2 is proper ) ; :: thesis: f1 is proper
dom (v .--> x) = dom {[v,x]} by FUNCT_4:82
.= {v} by RELAT_1:9 ;
then v in dom (v .--> x) by TARSKI:def 1;
then v in (dom f2) \/ (dom (v .--> x)) by XBOOLE_0:def 3;
then v in dom f1 by A1, FUNCT_4:def 1;
then A3: v in the_Vertices_of G1 ;
A4: ( not e in the_Edges_of G2 & w in the_Vertices_of G2 )

proof

assume ( e in the_Edges_of G2 or not w in the_Vertices_of G2 ) ; :: thesis: contradiction
then G1 == G2 by A1, GLIB_006:def 12;
hence contradiction by A1, A3, GLIB_000:def 34; :: thesis: verum

end;

now :: thesis: for e9, v9, w9 being object st e9 DJoins v9,w9,G1 holds
f1 . v9 <> f1 . w9

let e9, v9, w9 be object ; :: thesis: ( e9 DJoins v9,w9,G1 implies f1 . b₂ <> f1 . b₃ )
assume A5: e9 DJoins v9,w9,G1 ; :: thesis: f1 . b₂ <> f1 . b₃

per cases then ( e9 DJoins v9,w9,G2 or not e9 in the_Edges_of G2 ) by GLIB_006:71;

suppose A6: e9 DJoins v9,w9,G2 ; :: thesis: f1 . b₂ <> f1 . b₃

then e9 Joins v9,w9,G2 by GLIB_000:16;
then ( v9 <> v & w9 <> v ) by A1, GLIB_000:13;
then ( f1 . v9 = f2 . v9 & f1 . w9 = f2 . w9 ) by A1, FUNCT_4:83;
hence f1 . v9 <> f1 . w9 by A2, A6, Th11; :: thesis: verum

end;

suppose A7: not e9 in the_Edges_of G2 ; :: thesis: f1 . b₂ <> f1 . b₃

A8: the_Edges_of G1 = (the_Edges_of G2) \/ {e} by A1, A4, GLIB_006:def 12;
e9 in the_Edges_of G1 by A5, GLIB_000:def 14;
then e9 in {e} by A7, A8, XBOOLE_0:def 3;
then A9: e9 = e by TARSKI:def 1;
e DJoins v,w,G1 by A1, A4, GLIB_006:132;
then A10: ( v = v9 & w = w9 ) by A5, A9, GLIB_000:125;
( f1 . v = x & f1 . w = f2 . w ) by A1, A4, FUNCT_4:83, FUNCT_4:113;
hence f1 . v9 <> f1 . w9 by A2, A10; :: thesis: verum

end;

end;

end;

hence f1 is proper by Th11; :: thesis: verum