let V be set ; :: thesis: for c being Cardinal
for G2 being b₁ -ecolorable _Graph
for v being object
for G1 being addAdjVertexAll of G2,v,V holds G1 is c +` (card V) -ecolorable
let c be Cardinal; :: thesis: for G2 being c -ecolorable _Graph
for v being object
for G1 being addAdjVertexAll of G2,v,V holds G1 is c +` (card V) -ecolorable
let G2 be c -ecolorable _Graph; :: thesis: for v being object
for G1 being addAdjVertexAll of G2,v,V holds G1 is c +` (card V) -ecolorable
let v be object ; :: thesis: for G1 being addAdjVertexAll of G2,v,V holds G1 is c +` (card V) -ecolorable
let G1 be addAdjVertexAll of G2,v,V; :: thesis: G1 is c +` (card V) -ecolorable

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 A1: ( not v in the_Vertices_of G2 & V c= the_Vertices_of G2 ) ; :: thesis: G1 is c +` (card V) -ecolorable

consider g2 being proper EColoring of G2 such that
A2: card (rng g2) c= c by Def6;
consider E0 being set such that
A3: ( card V = card E0 & E0 misses the_Edges_of G2 ) and
A4: 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 A1, GLIB_007:def 4;
set E = G1 .edgesBetween (V,{v});
set h = <:((G1 .edgesBetween (V,{v})) --> (rng g2)),(id (G1 .edgesBetween (V,{v}))):>;
set g1 = g2 +* <:((G1 .edgesBetween (V,{v})) --> (rng g2)),(id (G1 .edgesBetween (V,{v}))):>;
A5: G1 .edgesBetween (V,{v}) = E0 by A1, A3, A4, GLIB_007:58;
dom <:((G1 .edgesBetween (V,{v})) --> (rng g2)),(id (G1 .edgesBetween (V,{v}))):> = G1 .edgesBetween (V,{v}) by Lm8;
then reconsider g1 = g2 +* <:((G1 .edgesBetween (V,{v})) --> (rng g2)),(id (G1 .edgesBetween (V,{v}))):> as EColoring of G1 by A1, Th82;
reconsider g1 = g1 as proper EColoring of G1 by A1, Th96;
card (rng g1) c= card ((rng g2) \/ (rng <:((G1 .edgesBetween (V,{v})) --> (rng g2)),(id (G1 .edgesBetween (V,{v}))):>)) by FUNCT_4:17, CARD_1:11;
then A6: card (rng g1) c= (card (rng g2)) +` (card (rng <:((G1 .edgesBetween (V,{v})) --> (rng g2)),(id (G1 .edgesBetween (V,{v}))):>)) by Lm11, CARD_2:35;
card (rng <:((G1 .edgesBetween (V,{v})) --> (rng g2)),(id (G1 .edgesBetween (V,{v}))):>) = card [:{(rng g2)},(G1 .edgesBetween (V,{v})):] by Lm10
.= card [:(G1 .edgesBetween (V,{v})),{(rng g2)}:] by CARD_2:4
.= card V by A3, A5, CARD_1:69 ;
then (card (rng g2)) +` (card (rng <:((G1 .edgesBetween (V,{v})) --> (rng g2)),(id (G1 .edgesBetween (V,{v}))):>)) c= c +` (card V) by A2, CARD_2:84;
hence G1 is c +` (card V) -ecolorable by A6, 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 +` (card V) -ecolorable

then G1 == G2 by GLIB_007:def 4;
then G1 is c -ecolorable by Th103;
hence G1 is c +` (card V) -ecolorable by Th99, CARD_2:94; :: thesis: verum

end;

end;