let G2 be _Graph; :: thesis: for v, e being object
for w being Vertex of G2
for G1 being addAdjVertex of G2,v,e,w
for t1 being TColoring of G1
for t2 being TColoring of G2
for x, y being object st not e in the_Edges_of G2 & not v in the_Vertices_of G2 & t1 _V = (t2 _V) +* (v .--> x) & t1 _E = (t2 _E) +* (e .--> y) & not y in (rng (t2 _V)) \/ (rng (t2 _E)) & x <> y & x <> (t2 _V) . w & t2 is proper holds
t1 is proper
let v, e be object ; :: thesis: for w being Vertex of G2
for G1 being addAdjVertex of G2,v,e,w
for t1 being TColoring of G1
for t2 being TColoring of G2
for x, y being object st not e in the_Edges_of G2 & not v in the_Vertices_of G2 & t1 _V = (t2 _V) +* (v .--> x) & t1 _E = (t2 _E) +* (e .--> y) & not y in (rng (t2 _V)) \/ (rng (t2 _E)) & x <> y & x <> (t2 _V) . w & t2 is proper holds
t1 is proper
let w be Vertex of G2; :: thesis: for G1 being addAdjVertex of G2,v,e,w
for t1 being TColoring of G1
for t2 being TColoring of G2
for x, y being object st not e in the_Edges_of G2 & not v in the_Vertices_of G2 & t1 _V = (t2 _V) +* (v .--> x) & t1 _E = (t2 _E) +* (e .--> y) & not y in (rng (t2 _V)) \/ (rng (t2 _E)) & x <> y & x <> (t2 _V) . w & t2 is proper holds
t1 is proper
let G1 be addAdjVertex of G2,v,e,w; :: thesis: for t1 being TColoring of G1
for t2 being TColoring of G2
for x, y being object st not e in the_Edges_of G2 & not v in the_Vertices_of G2 & t1 _V = (t2 _V) +* (v .--> x) & t1 _E = (t2 _E) +* (e .--> y) & not y in (rng (t2 _V)) \/ (rng (t2 _E)) & x <> y & x <> (t2 _V) . w & t2 is proper holds
t1 is proper
let t1 be TColoring of G1; :: thesis: for t2 being TColoring of G2
for x, y being object st not e in the_Edges_of G2 & not v in the_Vertices_of G2 & t1 _V = (t2 _V) +* (v .--> x) & t1 _E = (t2 _E) +* (e .--> y) & not y in (rng (t2 _V)) \/ (rng (t2 _E)) & x <> y & x <> (t2 _V) . w & t2 is proper holds
t1 is proper
let t2 be TColoring of G2; :: thesis: for x, y being object st not e in the_Edges_of G2 & not v in the_Vertices_of G2 & t1 _V = (t2 _V) +* (v .--> x) & t1 _E = (t2 _E) +* (e .--> y) & not y in (rng (t2 _V)) \/ (rng (t2 _E)) & x <> y & x <> (t2 _V) . w & t2 is proper holds
t1 is proper
let x, y be object ; :: thesis: ( not e in the_Edges_of G2 & not v in the_Vertices_of G2 & t1 _V = (t2 _V) +* (v .--> x) & t1 _E = (t2 _E) +* (e .--> y) & not y in (rng (t2 _V)) \/ (rng (t2 _E)) & x <> y & x <> (t2 _V) . w & t2 is proper implies t1 is proper )
assume that
A1: ( not e in the_Edges_of G2 & not v in the_Vertices_of G2 ) and
A2: ( t1 _V = (t2 _V) +* (v .--> x) & t1 _E = (t2 _E) +* (e .--> y) ) and
A3: ( not y in (rng (t2 _V)) \/ (rng (t2 _E)) & x <> y & x <> (t2 _V) . w & t2 is proper ) ; :: thesis: t1 is proper
A4: t1 _V is proper by A1, A2, A3, Th23;
not y in rng (t2 _E) by A3, XBOOLE_0:def 3;
then A5: t1 _E is proper by A1, A2, A3, Th94;

now :: thesis: for e9, v9, w9 being object st e9 Joins v9,w9,G1 holds
(t1 _V) . v9 <> (t1 _E) . e9

let e9, v9, w9 be object ; :: thesis: ( e9 Joins v9,w9,G1 implies (t1 _V) . b₂ <> (t1 _E) . b₁ )
assume A6: e9 Joins v9,w9,G1 ; :: thesis: (t1 _V) . b₂ <> (t1 _E) . b₁

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

suppose A7: e9 Joins v9,w9,G2 ; :: thesis: (t1 _V) . b₂ <> (t1 _E) . b₁

then e9 in the_Edges_of G2 by GLIB_000:def 13;
then not e9 in dom (e .--> y) by A1, TARSKI:def 1;
then A8: (t1 _E) . e9 = (t2 _E) . e9 by A2, FUNCT_4:11;
v9 in the_Vertices_of G2 by A7, GLIB_000:13;
then not v9 in dom (v .--> x) by A1, TARSKI:def 1;
then (t1 _V) . v9 = (t2 _V) . v9 by A2, FUNCT_4:11;
hence (t1 _V) . v9 <> (t1 _E) . e9 by A3, A7, A8, Th146; :: thesis: verum

end;

suppose A9: not e9 in the_Edges_of G2 ; :: thesis: (t1 _V) . b₂ <> (t1 _E) . b₁

A10: the_Edges_of G1 = (the_Edges_of G2) \/ {e} by A1, GLIB_006:def 12;
e9 in the_Edges_of G1 by A6, GLIB_000:def 13;
then e9 in {e} by A9, A10, XBOOLE_0:def 3;
then e9 = e by TARSKI:def 1;
then A11: (t1 _E) . e9 = y by A2, FUNCT_4:113;

per cases ( v9 = v or v9 <> v ) ;

suppose v9 = v ; :: thesis: (t1 _V) . b₂ <> (t1 _E) . b₁

hence (t1 _V) . v9 <> (t1 _E) . e9 by A2, A3, A11, FUNCT_4:113; :: thesis: verum

end;

suppose A12: v9 <> v ; :: thesis: (t1 _V) . b₂ <> (t1 _E) . b₁

then not v9 in dom (v .--> x) by TARSKI:def 1;
then A13: (t1 _V) . v9 = (t2 _V) . v9 by A2, FUNCT_4:11;
A14: the_Vertices_of G1 = (the_Vertices_of G2) \/ {v} by A1, GLIB_006:def 12;
( v9 in the_Vertices_of G1 & not v9 in {v} ) by A6, A12, GLIB_000:13, TARSKI:def 1;
then v9 in the_Vertices_of G2 by A14, XBOOLE_0:def 3;
then v9 in dom (t2 _V) by PARTFUN1:def 2;
then (t1 _V) . v9 in rng (t2 _V) by A13, FUNCT_1:3;
hence (t1 _V) . v9 <> (t1 _E) . e9 by A3, A11, XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

end;

end;

hence t1 is proper by A4, A5, Th146; :: thesis: verum