let G2 be _Graph; :: thesis: for v being object
for V being Subset of (the_Vertices_of G2)
for G1 being addAdjVertexAll of G2,v,V
for g2 being EColoring of G2
for g1 being EColoring of G1
for X, E being set st E = G1 .edgesBetween (V,{v}) & rng g2 c= X & g1 = g2 +* <:(E --> X),(id E):> & not v in the_Vertices_of G2 & g2 is proper holds
g1 is proper
let v be object ; :: thesis: for V being Subset of (the_Vertices_of G2)
for G1 being addAdjVertexAll of G2,v,V
for g2 being EColoring of G2
for g1 being EColoring of G1
for X, E being set st E = G1 .edgesBetween (V,{v}) & rng g2 c= X & g1 = g2 +* <:(E --> X),(id E):> & not v in the_Vertices_of G2 & g2 is proper holds
g1 is proper
let V be Subset of (the_Vertices_of G2); :: thesis: for G1 being addAdjVertexAll of G2,v,V
for g2 being EColoring of G2
for g1 being EColoring of G1
for X, E being set st E = G1 .edgesBetween (V,{v}) & rng g2 c= X & g1 = g2 +* <:(E --> X),(id E):> & not v in the_Vertices_of G2 & g2 is proper holds
g1 is proper
let G1 be addAdjVertexAll of G2,v,V; :: thesis: for g2 being EColoring of G2
for g1 being EColoring of G1
for X, E being set st E = G1 .edgesBetween (V,{v}) & rng g2 c= X & g1 = g2 +* <:(E --> X),(id E):> & not v in the_Vertices_of G2 & g2 is proper holds
g1 is proper
let g2 be EColoring of G2; :: thesis: for g1 being EColoring of G1
for X, E being set st E = G1 .edgesBetween (V,{v}) & rng g2 c= X & g1 = g2 +* <:(E --> X),(id E):> & not v in the_Vertices_of G2 & g2 is proper holds
g1 is proper
let g1 be EColoring of G1; :: thesis: for X, E being set st E = G1 .edgesBetween (V,{v}) & rng g2 c= X & g1 = g2 +* <:(E --> X),(id E):> & not v in the_Vertices_of G2 & g2 is proper holds
g1 is proper
let X, E be set ; :: thesis: ( E = G1 .edgesBetween (V,{v}) & rng g2 c= X & g1 = g2 +* <:(E --> X),(id E):> & not v in the_Vertices_of G2 & g2 is proper implies g1 is proper )
set h = <:(E --> X),(id E):>;
assume A1: ( E = G1 .edgesBetween (V,{v}) & rng g2 c= X ) ; :: thesis: ( not g1 = g2 +* <:(E --> X),(id E):> or v in the_Vertices_of G2 or not g2 is proper or g1 is proper )
assume A2: ( g1 = g2 +* <:(E --> X),(id E):> & not v in the_Vertices_of G2 & g2 is proper ) ; :: thesis: g1 is proper
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
A5: 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;
A6: E = E0 by A1, A2, A3, A4, GLIB_007:58;
A7: dom <:(E --> X),(id E):> = E by Lm8;

now :: thesis: for w being Vertex of G1
for e1, e2 being object st e1 in w .edgesInOut() & e2 in w .edgesInOut() & g1 . e1 = g1 . e2 holds
e1 = e2

let w be Vertex of G1; :: thesis: for e1, e2 being object st e1 in w .edgesInOut() & e2 in w .edgesInOut() & g1 . e1 = g1 . e2 holds
b₄ = b₅
let e1, e2 be object ; :: thesis: ( e1 in w .edgesInOut() & e2 in w .edgesInOut() & g1 . e1 = g1 . e2 implies b₂ = b₃ )
assume A8: ( e1 in w .edgesInOut() & e2 in w .edgesInOut() & g1 . e1 = g1 . e2 ) ; :: thesis: b₂ = b₃
consider u1 being Vertex of G1 such that
A9: e1 Joins w,u1,G1 by A8, GLIB_000:64;
consider u2 being Vertex of G1 such that
A10: e2 Joins w,u2,G1 by A8, GLIB_000:64;

per cases ( ( w <> v & not w in V ) or w = v or ( w <> v & w in V ) ) ;

suppose A11: ( w <> v & not w in V ) ; :: thesis: b₂ = b₃

then A12: ( not w in {v} & w in the_Vertices_of G1 ) by TARSKI:def 1;
the_Vertices_of G1 = (the_Vertices_of G2) \/ {v} by A2, GLIB_007:def 4;
then reconsider w2 = w as Vertex of G2 by A12, XBOOLE_0:def 3;
A13: w .edgesInOut() = w2 .edgesInOut() by A11, GLIBPRE0:56;
then ( not e1 in E & not e2 in E ) by A3, A6, A8, XBOOLE_0:3;
then ( g1 . e1 = g2 . e1 & g1 . e2 = g2 . e2 ) by A2, A7, FUNCT_4:11;
hence e1 = e2 by A2, A8, A13, Th85; :: thesis: verum

end;

suppose A14: w = v ; :: thesis: b₂ = b₃

A15: ( e1 Joins u1,v,G1 & e2 Joins u2,v,G1 ) by A14, A9, A10, GLIB_000:14;
then A16: ( u1 in V & u2 in V ) by A2, GLIB_007:def 4;
v in {v} by TARSKI:def 1;
then ( e1 SJoins V,{v},G1 & e2 SJoins V,{v},G1 ) by A15, A16, GLIB_000:17;
then A17: ( e1 in E & e2 in E ) by A1, GLIB_000:def 30;
A18: g1 . e1 = <:(E --> X),(id E):> . e1 by A2, A7, A17, FUNCT_4:13
.= [X,e1] by A17, Lm9 ;
g1 . e2 = <:(E --> X),(id E):> . e2 by A2, A7, A17, FUNCT_4:13
.= [X,e2] by A17, Lm9 ;
hence e1 = e2 by A8, A18, XTUPLE_0:1; :: thesis: verum

end;

suppose A19: ( w <> v & w in V ) ; :: thesis: b₂ = b₃

per cases ( ( e1 in E & e2 in E ) or ( e1 in E & not e2 in E ) or ( not e1 in E & e2 in E ) or ( not e1 in E & not e2 in E ) ) ;

suppose A20: ( e1 in E & e2 in E ) ; :: thesis: b₂ = b₃

then e1 SJoins V,{v},G1 by A1, GLIB_000:def 30;
then consider x1 being object such that
A21: ( x1 in V & e1 Joins x1,v,G1 ) by GLIB_000:102;
e2 SJoins V,{v},G1 by A1, A20, GLIB_000:def 30;
then consider x2 being object such that
A22: ( x2 in V & e2 Joins x2,v,G1 ) by GLIB_000:102;
A23: ( u1 = v & u2 = v ) by A9, A10, A19, A21, A22, GLIB_000:15;
consider e9 being object such that
( e9 in E0 & e9 Joins w,v,G1 ) and
A24: for e8 being object st e8 Joins w,v,G1 holds
e8 = e9 by A5, A19;
( e1 = e9 & e2 = e9 ) by A9, A10, A23, A24;
hence e1 = e2 ; :: thesis: verum

end;

suppose A25: ( e1 in E & not e2 in E ) ; :: thesis: b₂ = b₃

then A26: ( g1 . e1 = <:(E --> X),(id E):> . e1 & g1 . e2 = g2 . e2 ) by A2, A7, FUNCT_4:11, FUNCT_4:13;
e2 in the_Edges_of G1 by A10, GLIB_000:def 13;
then e2 in the_Edges_of G2 by A4, A6, A25, XBOOLE_0:def 3;
then e2 in dom g2 by PARTFUN1:def 2;
then ( g1 . e1 in rng <:(E --> X),(id E):> & g1 . e2 in rng g2 ) by A7, A25, A26, FUNCT_1:3;
hence e1 = e2 by A1, A8, Lm11, XBOOLE_0:3; :: thesis: verum

end;

suppose A27: ( not e1 in E & e2 in E ) ; :: thesis: b₂ = b₃

then A28: ( g1 . e1 = g2 . e1 & g1 . e2 = <:(E --> X),(id E):> . e2 ) by A2, A7, FUNCT_4:11, FUNCT_4:13;
e1 in the_Edges_of G1 by A9, GLIB_000:def 13;
then e1 in the_Edges_of G2 by A4, A6, A27, XBOOLE_0:def 3;
then e1 in dom g2 by PARTFUN1:def 2;
then ( g1 . e1 in rng g2 & g1 . e2 in rng <:(E --> X),(id E):> ) by A7, A27, A28, FUNCT_1:3;
hence e1 = e2 by A1, A8, Lm11, XBOOLE_0:3; :: thesis: verum

end;

suppose A29: ( not e1 in E & not e2 in E ) ; :: thesis: b₂ = b₃

then A30: ( g1 . e1 = g2 . e1 & g1 . e2 = g2 . e2 ) by A2, A7, FUNCT_4:11;
( e1 in the_Edges_of G2 & e2 in the_Edges_of G2 ) by A4, A6, A8, A29, XBOOLE_0:def 3;
then ( e1 Joins w,u1,G2 & e2 Joins w,u2,G2 ) by A9, A10, GLIB_006:72;
hence e1 = e2 by A2, A8, A30, Th86; :: thesis: verum

end;

end;

end;

end;

end;

hence g1 is proper by Th85; :: thesis: verum