let G2 be _Graph; :: thesis: for v, x being object
for V being Subset of (the_Vertices_of G2)
for G1 being addAdjVertexAll of G2,v,V
for f1 being VColoring of G1
for f2 being VColoring of G2 st not v in the_Vertices_of G2 & f1 = f2 +* (v .--> x) & not x in rng f2 & f2 is proper holds
f1 is proper
let v, x be object ; :: thesis: for V being Subset of (the_Vertices_of G2)
for G1 being addAdjVertexAll of G2,v,V
for f1 being VColoring of G1
for f2 being VColoring of G2 st not v in the_Vertices_of G2 & f1 = f2 +* (v .--> x) & not x in rng f2 & f2 is proper holds
f1 is proper
let V be Subset of (the_Vertices_of G2); :: thesis: for G1 being addAdjVertexAll of G2,v,V
for f1 being VColoring of G1
for f2 being VColoring of G2 st not v in the_Vertices_of G2 & f1 = f2 +* (v .--> x) & not x in rng f2 & f2 is proper holds
f1 is proper
let G1 be addAdjVertexAll of G2,v,V; :: thesis: for f1 being VColoring of G1
for f2 being VColoring of G2 st not v in the_Vertices_of G2 & f1 = f2 +* (v .--> x) & not x in rng f2 & f2 is proper holds
f1 is proper
let f1 be VColoring of G1; :: thesis: for f2 being VColoring of G2 st not v in the_Vertices_of G2 & f1 = f2 +* (v .--> x) & not x in rng f2 & f2 is proper holds
f1 is proper
let f2 be VColoring of G2; :: thesis: ( not v in the_Vertices_of G2 & f1 = f2 +* (v .--> x) & not x in rng f2 & f2 is proper implies f1 is proper )
set h = v .--> x;
assume A1: ( not v in the_Vertices_of G2 & f1 = f2 +* (v .--> x) & not x in rng f2 ) ; :: thesis: ( not f2 is proper or f1 is proper )
then A2: the_Vertices_of G1 = (the_Vertices_of G2) \/ {v} by GLIB_007:def 4;
assume A3: f2 is proper ; :: thesis: f1 is proper

now :: thesis: for e, u, w being object st e Joins u,w,G1 holds
f1 . u <> f1 . w

let e, u, w be object ; :: thesis: ( e Joins u,w,G1 implies f1 . b₂ <> f1 . b₃ )
assume A4: e Joins u,w,G1 ; :: thesis: f1 . b₂ <> f1 . b₃

per cases ( ( u <> v & w <> v ) or u = v or w = v ) ;

suppose A5: ( u <> v & w <> v ) ; :: thesis: f1 . b₂ <> f1 . b₃

then A6: e Joins u,w,G2 by A1, A4, GLIB_007:49;
( f1 . u = f2 . u & f1 . w = f2 . w ) by A1, A5, FUNCT_4:83;
hence f1 . u <> f1 . w by A3, A6, Th10; :: thesis: verum

end;

suppose A7: u = v ; :: thesis: f1 . b₂ <> f1 . b₃

then A8: w <> v by A1, A4, GLIB_007:def 4;
then A9: ( f1 . u = x & f1 . w = f2 . w ) by A1, A7, FUNCT_4:83, FUNCT_4:113;
w in the_Vertices_of G1 by A4, GLIB_000:13;
then w in the_Vertices_of G2 by A2, A8, ZFMISC_1:136;
then w in dom f2 by PARTFUN1:def 2;
hence f1 . u <> f1 . w by A1, A9, FUNCT_1:3; :: thesis: verum

end;

suppose A10: w = v ; :: thesis: f1 . b₂ <> f1 . b₃

then A11: u <> v by A1, A4, GLIB_007:def 4;
then A12: ( f1 . w = x & f1 . u = f2 . u ) by A1, A10, FUNCT_4:83, FUNCT_4:113;
u in the_Vertices_of G1 by A4, GLIB_000:13;
then u in the_Vertices_of G2 by A2, A11, ZFMISC_1:136;
then u in dom f2 by PARTFUN1:def 2;
hence f1 . u <> f1 . w by A1, A12, FUNCT_1:3; :: thesis: verum

end;

end;

end;

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