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 f1 being VColoring of G1
for f2 being VColoring of G2
for x being object st f1 = f2 +* (w .--> x) & v <> w & not x in rng f2 & f2 is proper holds
f1 is proper
let v, e be object ; :: thesis: for w being Vertex of G2
for G1 being addEdge of G2,v,e,w
for f1 being VColoring of G1
for f2 being VColoring of G2
for x being object st f1 = f2 +* (w .--> x) & v <> w & not x in rng f2 & f2 is proper holds
f1 is proper
let w be Vertex of G2; :: thesis: for G1 being addEdge of G2,v,e,w
for f1 being VColoring of G1
for f2 being VColoring of G2
for x being object st f1 = f2 +* (w .--> x) & v <> w & not x in rng f2 & f2 is proper holds
f1 is proper
let G1 be addEdge of G2,v,e,w; :: thesis: for f1 being VColoring of G1
for f2 being VColoring of G2
for x being object st f1 = f2 +* (w .--> x) & v <> w & not x in rng f2 & f2 is proper holds
f1 is proper
let f1 be VColoring of G1; :: thesis: for f2 being VColoring of G2
for x being object st f1 = f2 +* (w .--> x) & v <> w & not x in rng f2 & f2 is proper holds
f1 is proper
let f2 be VColoring of G2; :: thesis: for x being object st f1 = f2 +* (w .--> x) & v <> w & not x in rng f2 & f2 is proper holds
f1 is proper
let x be object ; :: thesis: ( f1 = f2 +* (w .--> x) & v <> w & not x in rng f2 & f2 is proper implies f1 is proper )
assume A1: ( f1 = f2 +* (w .--> x) & v <> w & not x in rng f2 & f2 is proper ) ; :: thesis: f1 is proper

per cases ( not e in the_Edges_of G2 or e in the_Edges_of G2 ) ;

suppose A2: not e in the_Edges_of G2 ; :: thesis: f1 is proper

set G3 = the reverseEdgeDirections of G1,{e};
A3: the reverseEdgeDirections of G1,{e} is addEdge of G2,w,e,v by A2, GLIBPRE1:65;
the_Vertices_of G1 = the_Vertices_of the reverseEdgeDirections of G1,{e} by GLIB_007:4;
then reconsider f3 = f1 as VColoring of the reverseEdgeDirections of G1,{e} ;
f3 is proper by A1, A3, Th21;
hence f1 is proper by Th18; :: thesis: verum

end;

suppose e in the_Edges_of G2 ; :: thesis: f1 is proper

then G1 == G2 by GLIB_006:def 11;
hence f1 is proper by A1, Th17; :: thesis: verum

end;

end;