let G2 be _Graph; :: thesis: for v, e being object
for w being Vertex of G2
for G1 being addEdge 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 & v <> w & t1 _V = (t2 _V) +* (v .--> x) & t1 _E = (t2 _E) +* (e .--> y) & {x,y} misses (rng (t2 _V)) \/ (rng (t2 _E)) & x <> y & t2 is proper holds
t1 is proper
let v, e be object ; :: thesis: for w being Vertex of G2
for G1 being addEdge 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 & v <> w & t1 _V = (t2 _V) +* (v .--> x) & t1 _E = (t2 _E) +* (e .--> y) & {x,y} misses (rng (t2 _V)) \/ (rng (t2 _E)) & x <> y & t2 is proper holds
t1 is proper
let w be Vertex of G2; :: thesis: for G1 being addEdge 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 & v <> w & t1 _V = (t2 _V) +* (v .--> x) & t1 _E = (t2 _E) +* (e .--> y) & {x,y} misses (rng (t2 _V)) \/ (rng (t2 _E)) & x <> y & t2 is proper holds
t1 is proper
let G1 be addEdge 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 & v <> w & t1 _V = (t2 _V) +* (v .--> x) & t1 _E = (t2 _E) +* (e .--> y) & {x,y} misses (rng (t2 _V)) \/ (rng (t2 _E)) & x <> y & 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 & v <> w & t1 _V = (t2 _V) +* (v .--> x) & t1 _E = (t2 _E) +* (e .--> y) & {x,y} misses (rng (t2 _V)) \/ (rng (t2 _E)) & x <> y & 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 & v <> w & t1 _V = (t2 _V) +* (v .--> x) & t1 _E = (t2 _E) +* (e .--> y) & {x,y} misses (rng (t2 _V)) \/ (rng (t2 _E)) & x <> y & t2 is proper holds
t1 is proper
let x, y be object ; :: thesis: ( not e in the_Edges_of G2 & v <> w & t1 _V = (t2 _V) +* (v .--> x) & t1 _E = (t2 _E) +* (e .--> y) & {x,y} misses (rng (t2 _V)) \/ (rng (t2 _E)) & x <> y & t2 is proper implies t1 is proper )
assume that
A1: ( not e in the_Edges_of G2 & v <> w ) and
A2: ( t1 _V = (t2 _V) +* (v .--> x) & t1 _E = (t2 _E) +* (e .--> y) ) and
A3: ( {x,y} misses (rng (t2 _V)) \/ (rng (t2 _E)) & x <> y & t2 is proper ) ; :: thesis: t1 is proper
A4: dom (v .--> x) = dom {[v,x]} by FUNCT_4:82
.= {v} by RELAT_1:9 ;
A5: v in the_Vertices_of G2

proof

per cases ( G1 != G2 or G1 == G2 ) ;

suppose G1 != G2 ; :: thesis: v in the_Vertices_of G2

hence v in the_Vertices_of G2 by GLIB_006:def 11; :: thesis: verum

end;

suppose A6: G1 == G2 ; :: thesis: v in the_Vertices_of G2

v in dom (v .--> x) by A4, TARSKI:def 1;
then v in (dom (t2 _V)) \/ (dom (v .--> x)) by XBOOLE_0:def 3;
then v in dom (t1 _V) by A2, FUNCT_4:def 1;
then v in the_Vertices_of G1 ;
hence v in the_Vertices_of G2 by A6, GLIB_000:def 34; :: thesis: verum

end;

end;

end;

{x,y} misses rng (t2 _V) by A3, XBOOLE_1:7, XBOOLE_1:63;
then A7: t1 _V is proper by A1, A2, A3, A5, Th21, ZFMISC_1:49;
{x,y} misses rng (t2 _E) by A3, XBOOLE_1:7, XBOOLE_1:63;
then not y in rng (t2 _E) by ZFMISC_1:49;
then A8: t1 _E is proper by A1, A2, A3, Th93;

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 A9: 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 A10: e9 Joins v9,w9,G2 ; :: thesis: (t1 _V) . b₂ <> (t1 _E) . b₁

then A11: e9 in the_Edges_of G2 by GLIB_000:def 13;
then not e9 in dom (e .--> y) by A1, TARSKI:def 1;
then A12: (t1 _E) . e9 = (t2 _E) . e9 by A2, FUNCT_4:11;

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

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

then A13: (t1 _V) . v9 = x by A2, FUNCT_4:113;
e9 in dom (t2 _E) by A11, PARTFUN1:def 2;
then (t2 _E) . e9 in rng (t2 _E) by FUNCT_1:3;
then (t1 _E) . e9 in (rng (t2 _V)) \/ (rng (t2 _E)) by A12, XBOOLE_0:def 3;
hence (t1 _V) . v9 <> (t1 _E) . e9 by A3, A13, ZFMISC_1:49; :: thesis: verum

end;

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

then not v9 in dom (v .--> x) by TARSKI:def 1;
then (t1 _V) . v9 = (t2 _V) . v9 by A2, FUNCT_4:11;
hence (t1 _V) . v9 <> (t1 _E) . e9 by A3, A10, A12, Th146; :: thesis: verum

end;

end;

end;

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

then e9 = e by A1, A5, A9, GLIB_006:106;
then A14: (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, A14, FUNCT_4:113; :: thesis: verum

end;

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

then not v9 in dom (v .--> x) by TARSKI:def 1;
then A15: (t1 _V) . v9 = (t2 _V) . v9 by A2, FUNCT_4:11;
v9 in the_Vertices_of G1 by A9, GLIB_000:13;
then v9 in the_Vertices_of G2 by A5, GLIB_006:102;
then v9 in dom (t2 _V) by PARTFUN1:def 2;
then (t1 _V) . v9 in rng (t2 _V) by A15, FUNCT_1:3;
then (t1 _V) . v9 in (rng (t2 _V)) \/ (rng (t2 _E)) by XBOOLE_0:def 3;
hence (t1 _V) . v9 <> (t1 _E) . e9 by A3, A14, ZFMISC_1:49; :: thesis: verum

end;

end;

end;

end;

end;

hence t1 is proper by A7, A8, Th146; :: thesis: verum