let c be Cardinal; :: thesis: for G2 being non edgeless _Graph
for v being Vertex of G2
for e, w being object
for G1 being addAdjVertex of G2,v,e,w st not e in the_Edges_of G2 & not w in the_Vertices_of G2 & G2 is c -vcolorable holds
G1 is c -vcolorable
let G2 be non edgeless _Graph; :: thesis: for v being Vertex of G2
for e, w being object
for G1 being addAdjVertex of G2,v,e,w st not e in the_Edges_of G2 & not w in the_Vertices_of G2 & G2 is c -vcolorable holds
G1 is c -vcolorable
let v be Vertex of G2; :: thesis: for e, w being object
for G1 being addAdjVertex of G2,v,e,w st not e in the_Edges_of G2 & not w in the_Vertices_of G2 & G2 is c -vcolorable holds
G1 is c -vcolorable
let e, w be object ; :: thesis: for G1 being addAdjVertex of G2,v,e,w st not e in the_Edges_of G2 & not w in the_Vertices_of G2 & G2 is c -vcolorable holds
G1 is c -vcolorable
let G1 be addAdjVertex of G2,v,e,w; :: thesis: ( not e in the_Edges_of G2 & not w in the_Vertices_of G2 & G2 is c -vcolorable implies G1 is c -vcolorable )
assume A1: ( not e in the_Edges_of G2 & not w in the_Vertices_of G2 ) ; :: thesis: ( not G2 is c -vcolorable or G1 is c -vcolorable )
assume G2 is c -vcolorable ; :: thesis: G1 is c -vcolorable
then consider f2 being VColoring of G2 such that
A2: ( f2 is proper & card (rng f2) c= c ) ;
set e0 = the Element of the_Edges_of G2;
set x = the Element of (rng f2) \ {(f2 . v)};
(rng f2) \ {(f2 . v)} <> {}

proof

assume (rng f2) \ {(f2 . v)} = {} ; :: thesis: contradiction
then ( rng f2 = {} or rng f2 = {(f2 . v)} ) by ZFMISC_1:58;
then ( card (rng f2) = 0 or card (rng f2) = 1 ) by CARD_1:30;
then ( G2 is 0 -vcolorable or G2 is 1 -vcolorable ) by A2;
hence contradiction ; :: thesis: verum

end;

then A3: ( the Element of (rng f2) \ {(f2 . v)} in rng f2 & the Element of (rng f2) \ {(f2 . v)} <> f2 . v ) by ZFMISC_1:56;
set h = w .--> the Element of (rng f2) \ {(f2 . v)};
set f1 = f2 +* (w .--> the Element of (rng f2) \ {(f2 . v)});
reconsider f1 = f2 +* (w .--> the Element of (rng f2) \ {(f2 . v)}) as VColoring of G1 by A1, Th6;
A4: f1 is proper by A1, A2, A3, Th24;
(rng f2) \/ (rng (w .--> the Element of (rng f2) \ {(f2 . v)})) = (rng f2) \/ (rng {[w, the Element of (rng f2) \ {(f2 . v)}]}) by FUNCT_4:82
.= (rng f2) \/ { the Element of (rng f2) \ {(f2 . v)}} by RELAT_1:9
.= rng f2 by A3, ZFMISC_1:40 ;
then card (rng f1) c= card (rng f2) by FUNCT_4:17, CARD_1:11;
hence G1 is c -vcolorable by A2, A4, XBOOLE_1:1; :: thesis: verum