let V be set ; :: thesis: for G2 being _Graph
for c being Cardinal
for v being object
for G1 being addAdjVertexAll of G2,v,V st G2 is c -tcolorable holds
G1 is (c +` 1) +` (card V) -tcolorable
let G2 be _Graph; :: thesis: for c being Cardinal
for v being object
for G1 being addAdjVertexAll of G2,v,V st G2 is c -tcolorable holds
G1 is (c +` 1) +` (card V) -tcolorable
let c be Cardinal; :: thesis: for v being object
for G1 being addAdjVertexAll of G2,v,V st G2 is c -tcolorable holds
G1 is (c +` 1) +` (card V) -tcolorable
let v be object ; :: thesis: for G1 being addAdjVertexAll of G2,v,V st G2 is c -tcolorable holds
G1 is (c +` 1) +` (card V) -tcolorable
let G1 be addAdjVertexAll of G2,v,V; :: thesis: ( G2 is c -tcolorable implies G1 is (c +` 1) +` (card V) -tcolorable )
assume A1: G2 is c -tcolorable ; :: thesis: G1 is (c +` 1) +` (card V) -tcolorable

per cases ( ( not v in the_Vertices_of G2 & V c= the_Vertices_of G2 ) or v in the_Vertices_of G2 or not V c= the_Vertices_of G2 ) ;

suppose A2: ( not v in the_Vertices_of G2 & V c= the_Vertices_of G2 ) ; :: thesis: G1 is (c +` 1) +` (card V) -tcolorable

consider t0 being TColoring of G2 such that
A3: ( t0 is proper & card ((rng (t0 _V)) \/ (rng (t0 _E))) c= c ) by A1;
set R = (rng (t0 _V)) \/ (rng (t0 _E));
set E = G1 .edgesBetween (V,{v});
set h = <:((G1 .edgesBetween (V,{v})) --> ((rng (t0 _V)) \/ (rng (t0 _E)))),(id (G1 .edgesBetween (V,{v}))):>;
set g = (t0 _E) +* <:((G1 .edgesBetween (V,{v})) --> ((rng (t0 _V)) \/ (rng (t0 _E)))),(id (G1 .edgesBetween (V,{v}))):>;
set f = (t0 _V) +* (v .--> ((rng (t0 _V)) \/ (rng (t0 _E))));
A4: ( dom <:((G1 .edgesBetween (V,{v})) --> ((rng (t0 _V)) \/ (rng (t0 _E)))),(id (G1 .edgesBetween (V,{v}))):> = G1 .edgesBetween (V,{v}) & rng (t0 _E) c= (rng (t0 _V)) \/ (rng (t0 _E)) ) by Lm8, XBOOLE_1:7;
then reconsider g = (t0 _E) +* <:((G1 .edgesBetween (V,{v})) --> ((rng (t0 _V)) \/ (rng (t0 _E)))),(id (G1 .edgesBetween (V,{v}))):> as EColoring of G1 by A2, Th82;
reconsider f = (t0 _V) +* (v .--> ((rng (t0 _V)) \/ (rng (t0 _E)))) as VColoring of G1 by A2, Th7;
reconsider g = g as proper EColoring of G1 by A2, A3, A4, Th96;
reconsider t = [f,g] as TColoring of G1 ;
not (rng (t0 _V)) \/ (rng (t0 _E)) in rng (t0 _V)

proof

assume A5: (rng (t0 _V)) \/ (rng (t0 _E)) in rng (t0 _V) ; :: thesis: contradiction
rng (t0 _V) c= (rng (t0 _V)) \/ (rng (t0 _E)) by XBOOLE_1:7;
then (rng (t0 _V)) \/ (rng (t0 _E)) in (rng (t0 _V)) \/ (rng (t0 _E)) by A5;
hence contradiction ; :: thesis: verum

end;

then A6: t _V is proper by A2, A3, Th25;

now :: thesis: for e, u, w being object st e Joins u,w,G1 holds
not (t _V) . u = (t _E) . e

let e, u, w be object ; :: thesis: ( e Joins u,w,G1 implies not (t _V) . b₂ = (t _E) . b₁ )
assume A7: e Joins u,w,G1 ; :: thesis: not (t _V) . b₂ = (t _E) . b₁

per cases ( not e in the_Edges_of G2 or e Joins u,w,G2 ) by A7, GLIB_006:72;

suppose A8: not e in the_Edges_of G2 ; :: thesis: not (t _V) . b₂ = (t _E) . b₁

A9: the_Edges_of G1 = (the_Edges_of G2) \/ (G1 .edgesBetween (V,{v})) by A2, GLIB_007:59;
e in the_Edges_of G1 by A7, GLIB_000:def 13;
then A10: e in G1 .edgesBetween (V,{v}) by A8, A9, XBOOLE_0:def 3;
then e SJoins V,{v},G1 by GLIB_000:def 30;
then consider x being object such that
A11: ( x in V & e Joins x,v,G1 ) by GLIB_000:102;
A12: x <> v by A2, A11;
e in dom <:((G1 .edgesBetween (V,{v})) --> ((rng (t0 _V)) \/ (rng (t0 _E)))),(id (G1 .edgesBetween (V,{v}))):> by A10, Lm8;
then A13: (t _E) . e = <:((G1 .edgesBetween (V,{v})) --> ((rng (t0 _V)) \/ (rng (t0 _E)))),(id (G1 .edgesBetween (V,{v}))):> . e by FUNCT_4:13
.= [((rng (t0 _V)) \/ (rng (t0 _E))),e] by A10, Lm9 ;

per cases ( ( u = x & w = v ) or ( u = v & w = x ) ) by A7, A11, GLIB_000:15;

suppose A14: ( u = x & w = v ) ; :: thesis: not (t _V) . b₂ = (t _E) . b₁

then A15: (t _V) . u = (t0 _V) . u by A12, FUNCT_4:83;
u in the_Vertices_of G2 by A2, A11, A14;
then u in dom (t0 _V) by PARTFUN1:def 2;
then A16: (t0 _V) . u in rng (t0 _V) by FUNCT_1:3;
assume (t _V) . u = (t _E) . e ; :: thesis: contradiction
then A17: [((rng (t0 _V)) \/ (rng (t0 _E))),e] in rng (t0 _V) by A13, A15, A16;
rng (t0 _V) c= (rng (t0 _V)) \/ (rng (t0 _E)) by XBOOLE_1:7;
then [((rng (t0 _V)) \/ (rng (t0 _E))),e] in (rng (t0 _V)) \/ (rng (t0 _E)) by A17;
then A18: {{((rng (t0 _V)) \/ (rng (t0 _E))),e},{((rng (t0 _V)) \/ (rng (t0 _E)))}} in (rng (t0 _V)) \/ (rng (t0 _E)) by TARSKI:def 5;
A19: (rng (t0 _V)) \/ (rng (t0 _E)) in {((rng (t0 _V)) \/ (rng (t0 _E)))} by TARSKI:def 1;
{((rng (t0 _V)) \/ (rng (t0 _E)))} in {{((rng (t0 _V)) \/ (rng (t0 _E))),e},{((rng (t0 _V)) \/ (rng (t0 _E)))}} by TARSKI:def 2;
hence contradiction by A18, A19, XREGULAR:7; :: thesis: verum

end;

suppose ( u = v & w = x ) ; :: thesis: not (t _V) . b₂ = (t _E) . b₁

then A20: (t _V) . u = (rng (t0 _V)) \/ (rng (t0 _E)) by FUNCT_4:113;
assume (t _V) . u = (t _E) . e ; :: thesis: contradiction
then (rng (t0 _V)) \/ (rng (t0 _E)) = {{((rng (t0 _V)) \/ (rng (t0 _E))),e},{((rng (t0 _V)) \/ (rng (t0 _E)))}} by A13, A20, TARSKI:def 5;
then ( (rng (t0 _V)) \/ (rng (t0 _E)) in {((rng (t0 _V)) \/ (rng (t0 _E)))} & {((rng (t0 _V)) \/ (rng (t0 _E)))} in (rng (t0 _V)) \/ (rng (t0 _E)) ) by TARSKI:def 1, TARSKI:def 2;
hence contradiction ; :: thesis: verum

end;

end;

end;

suppose A21: e Joins u,w,G2 ; :: thesis: (t _V) . b₂ <> (t _E) . b₁

then A22: (t0 _V) . u <> (t0 _E) . e by A3, Th146;
A23: ( e in the_Edges_of G2 & u in the_Vertices_of G2 ) by A21, GLIB_000:def 13, GLIB_000:13;
the_Edges_of G2 misses G1 .edgesBetween (V,{v}) by A2, GLIB_007:59;
then not e in G1 .edgesBetween (V,{v}) by A23, XBOOLE_0:3;
then not e in dom <:((G1 .edgesBetween (V,{v})) --> ((rng (t0 _V)) \/ (rng (t0 _E)))),(id (G1 .edgesBetween (V,{v}))):> by Lm8;
then A24: (t _E) . e = (t0 _E) . e by FUNCT_4:11;
(t _V) . u = (t0 _V) . u by A2, A23, FUNCT_4:83;
hence (t _V) . u <> (t _E) . e by A22, A24; :: thesis: verum

end;

end;

end;

then A25: t is proper by A6, Th146;
(rng (t0 _V)) \/ (rng (v .--> ((rng (t0 _V)) \/ (rng (t0 _E))))) = (rng (t0 _V)) \/ (rng {[v,((rng (t0 _V)) \/ (rng (t0 _E)))]}) by FUNCT_4:82
.= (rng (t0 _V)) \/ {((rng (t0 _V)) \/ (rng (t0 _E)))} by RELAT_1:9 ;
then A26: rng f c= (rng (t0 _V)) \/ {((rng (t0 _V)) \/ (rng (t0 _E)))} by FUNCT_4:17;
A27: rng g c= (rng (t0 _E)) \/ (rng <:((G1 .edgesBetween (V,{v})) --> ((rng (t0 _V)) \/ (rng (t0 _E)))),(id (G1 .edgesBetween (V,{v}))):>) by FUNCT_4:17;
((rng (t0 _V)) \/ {((rng (t0 _V)) \/ (rng (t0 _E)))}) \/ ((rng (t0 _E)) \/ (rng <:((G1 .edgesBetween (V,{v})) --> ((rng (t0 _V)) \/ (rng (t0 _E)))),(id (G1 .edgesBetween (V,{v}))):>)) = (((rng (t0 _V)) \/ {((rng (t0 _V)) \/ (rng (t0 _E)))}) \/ (rng (t0 _E))) \/ (rng <:((G1 .edgesBetween (V,{v})) --> ((rng (t0 _V)) \/ (rng (t0 _E)))),(id (G1 .edgesBetween (V,{v}))):>) by XBOOLE_1:4
.= (((rng (t0 _V)) \/ (rng (t0 _E))) \/ {((rng (t0 _V)) \/ (rng (t0 _E)))}) \/ (rng <:((G1 .edgesBetween (V,{v})) --> ((rng (t0 _V)) \/ (rng (t0 _E)))),(id (G1 .edgesBetween (V,{v}))):>) by XBOOLE_1:4 ;
then (rng f) \/ (rng g) c= (((rng (t0 _V)) \/ (rng (t0 _E))) \/ {((rng (t0 _V)) \/ (rng (t0 _E)))}) \/ (rng <:((G1 .edgesBetween (V,{v})) --> ((rng (t0 _V)) \/ (rng (t0 _E)))),(id (G1 .edgesBetween (V,{v}))):>) by A26, A27, XBOOLE_1:13;
then A28: card ((rng f) \/ (rng g)) c= card ((((rng (t0 _V)) \/ (rng (t0 _E))) \/ {((rng (t0 _V)) \/ (rng (t0 _E)))}) \/ (rng <:((G1 .edgesBetween (V,{v})) --> ((rng (t0 _V)) \/ (rng (t0 _E)))),(id (G1 .edgesBetween (V,{v}))):>)) by CARD_1:11;
not (rng (t0 _V)) \/ (rng (t0 _E)) in (rng (t0 _V)) \/ (rng (t0 _E)) ;
then A29: (rng (t0 _V)) \/ (rng (t0 _E)) misses {((rng (t0 _V)) \/ (rng (t0 _E)))} by ZFMISC_1:50;
A30: card (G1 .edgesBetween (V,{v})) = card V

proof

consider E0 being set such that
A31: ( card V = card E0 & E0 misses the_Edges_of G2 ) and
A32: the_Edges_of G1 = (the_Edges_of G2) \/ E0 and
for v1 being object st v1 in V holds
ex e1 being object st
( e1 in E0 & e1 Joins v1,v,G1 & ( for e2 being object st e2 Joins v1,v,G1 holds
e1 = e2 ) ) by A2, GLIB_007:def 4;
thus card (G1 .edgesBetween (V,{v})) = card V by A2, A31, A32, GLIB_007:58; :: thesis: verum

end;

card ((((rng (t0 _V)) \/ (rng (t0 _E))) \/ {((rng (t0 _V)) \/ (rng (t0 _E)))}) \/ (rng <:((G1 .edgesBetween (V,{v})) --> ((rng (t0 _V)) \/ (rng (t0 _E)))),(id (G1 .edgesBetween (V,{v}))):>)) = (card (((rng (t0 _V)) \/ (rng (t0 _E))) \/ {((rng (t0 _V)) \/ (rng (t0 _E)))})) +` (card (rng <:((G1 .edgesBetween (V,{v})) --> ((rng (t0 _V)) \/ (rng (t0 _E)))),(id (G1 .edgesBetween (V,{v}))):>)) by Lm21, CARD_2:35
.= ((card ((rng (t0 _V)) \/ (rng (t0 _E)))) +` (card {((rng (t0 _V)) \/ (rng (t0 _E)))})) +` (card (rng <:((G1 .edgesBetween (V,{v})) --> ((rng (t0 _V)) \/ (rng (t0 _E)))),(id (G1 .edgesBetween (V,{v}))):>)) by A29, CARD_2:35
.= ((card ((rng (t0 _V)) \/ (rng (t0 _E)))) +` 1) +` (card (rng <:((G1 .edgesBetween (V,{v})) --> ((rng (t0 _V)) \/ (rng (t0 _E)))),(id (G1 .edgesBetween (V,{v}))):>)) by CARD_1:30
.= ((card ((rng (t0 _V)) \/ (rng (t0 _E)))) +` 1) +` (card [:{((rng (t0 _V)) \/ (rng (t0 _E)))},(G1 .edgesBetween (V,{v})):]) by Lm10
.= ((card ((rng (t0 _V)) \/ (rng (t0 _E)))) +` 1) +` (card [:(G1 .edgesBetween (V,{v})),{((rng (t0 _V)) \/ (rng (t0 _E)))}:]) by CARD_2:4
.= ((card ((rng (t0 _V)) \/ (rng (t0 _E)))) +` 1) +` (card (G1 .edgesBetween (V,{v}))) by CARD_1:69
.= (card ((rng (t0 _V)) \/ (rng (t0 _E)))) +` (1 +` (card V)) by A30, CARD_2:19 ;
then card ((((rng (t0 _V)) \/ (rng (t0 _E))) \/ {((rng (t0 _V)) \/ (rng (t0 _E)))}) \/ (rng <:((G1 .edgesBetween (V,{v})) --> ((rng (t0 _V)) \/ (rng (t0 _E)))),(id (G1 .edgesBetween (V,{v}))):>)) c= c +` (1 +` (card V)) by A3, CARD_2:84;
then card ((((rng (t0 _V)) \/ (rng (t0 _E))) \/ {((rng (t0 _V)) \/ (rng (t0 _E)))}) \/ (rng <:((G1 .edgesBetween (V,{v})) --> ((rng (t0 _V)) \/ (rng (t0 _E)))),(id (G1 .edgesBetween (V,{v}))):>)) c= (c +` 1) +` (card V) by CARD_2:19;
hence G1 is (c +` 1) +` (card V) -tcolorable by A25, A28, XBOOLE_1:1; :: thesis: verum

end;

suppose ( v in the_Vertices_of G2 or not V c= the_Vertices_of G2 ) ; :: thesis: G1 is (c +` 1) +` (card V) -tcolorable

then G1 == G2 by GLIB_007:def 4;
then G1 is c -tcolorable by A1, Th167;
then G1 is c +` 1 -tcolorable by Th161, CARD_2:94;
hence G1 is (c +` 1) +` (card V) -tcolorable by Th161, CARD_2:94; :: thesis: verum

end;

end;