let G2 be _Graph; :: thesis: for v, e, w being object
for G1 being addEdge of G2,v,e,w
for g1 being EColoring of G1
for g2 being EColoring of G2
for x being object st g1 = g2 +* (e .--> x) & not e in the_Edges_of G2 & not x in rng g2 & g2 is proper holds
g1 is proper
let v, e, w be object ; :: thesis: for G1 being addEdge of G2,v,e,w
for g1 being EColoring of G1
for g2 being EColoring of G2
for x being object st g1 = g2 +* (e .--> x) & not e in the_Edges_of G2 & not x in rng g2 & g2 is proper holds
g1 is proper
let G1 be addEdge of G2,v,e,w; :: thesis: for g1 being EColoring of G1
for g2 being EColoring of G2
for x being object st g1 = g2 +* (e .--> x) & not e in the_Edges_of G2 & not x in rng g2 & g2 is proper holds
g1 is proper
let g1 be EColoring of G1; :: thesis: for g2 being EColoring of G2
for x being object st g1 = g2 +* (e .--> x) & not e in the_Edges_of G2 & not x in rng g2 & g2 is proper holds
g1 is proper
let g2 be EColoring of G2; :: thesis: for x being object st g1 = g2 +* (e .--> x) & not e in the_Edges_of G2 & not x in rng g2 & g2 is proper holds
g1 is proper
let x be object ; :: thesis: ( g1 = g2 +* (e .--> x) & not e in the_Edges_of G2 & not x in rng g2 & g2 is proper implies g1 is proper )
assume A1: ( g1 = g2 +* (e .--> x) & not e in the_Edges_of G2 ) ; :: thesis: ( x in rng g2 or not g2 is proper or g1 is proper )
assume A2: ( not x in rng g2 & g2 is proper ) ; :: thesis: g1 is proper
dom (e .--> x) = dom {[e,x]} by FUNCT_4:82
.= {e} by RELAT_1:9 ;
then e in dom (e .--> x) by TARSKI:def 1;
then e in (dom g2) \/ (dom (e .--> x)) by XBOOLE_0:def 3;
then e in dom g1 by A1, FUNCT_4:def 1;
then A3: e in the_Edges_of G1 ;
A4: rng (e .--> x) = rng {[e,x]} by FUNCT_4:82
.= {x} by RELAT_1:9 ;
A5: ( v is Vertex of G2 & w is Vertex of G2 )

proof

assume ( not v is Vertex of G2 or not w is Vertex of G2 ) ; :: thesis: contradiction
then G1 == G2 by GLIB_006:def 11;
hence contradiction by A1, A3, GLIB_000:def 34; :: thesis: verum

end;

now :: thesis: for u1 being Vertex of G1 holds g1 | (u1 .edgesInOut()) is one-to-one

let u1 be Vertex of G1; :: thesis: g1 | (b₁ .edgesInOut()) is one-to-one
A6: g1 | (u1 .edgesInOut()) = (g2 | (u1 .edgesInOut())) +* ((e .--> x) | (u1 .edgesInOut())) by A1, FUNCT_4:71;
reconsider u2 = u1 as Vertex of G2 by A1, A5, GLIB_006:def 11;

per cases ( ( u1 <> v & u1 <> w ) or u1 = v or u1 = w ) ;

suppose ( u1 <> v & u1 <> w ) ; :: thesis: g1 | (b₁ .edgesInOut()) is one-to-one

then A7: u1 .edgesInOut() = u2 .edgesInOut() by GLIBPRE0:46;
not e in u2 .edgesInOut() by A1;
then (e .--> x) | (u1 .edgesInOut()) = {} by A7, FUNCOP_1:76;
hence g1 | (u1 .edgesInOut()) is one-to-one by A2, A6, A7; :: thesis: verum

end;

suppose A8: ( u1 = v or u1 = w ) ; :: thesis: g1 | (b₁ .edgesInOut()) is one-to-one

A9: u1 .edgesInOut() = (u2 .edgesInOut()) \/ {e}

proof

per cases ( ( u1 = v & u1 <> w ) or ( u1 <> v & u1 = w ) or ( u1 = v & u1 = w ) ) by A8;

suppose ( u1 = v & u1 <> w ) ; :: thesis: u1 .edgesInOut() = (u2 .edgesInOut()) \/ {e}

hence u1 .edgesInOut() = (u2 .edgesInOut()) \/ {e} by A1, A5, GLIBPRE0:47; :: thesis: verum

end;

suppose ( u1 <> v & u1 = w ) ; :: thesis: u1 .edgesInOut() = (u2 .edgesInOut()) \/ {e}

hence u1 .edgesInOut() = (u2 .edgesInOut()) \/ {e} by A1, A5, GLIBPRE0:48; :: thesis: verum

end;

suppose ( u1 = v & u1 = w ) ; :: thesis: u1 .edgesInOut() = (u2 .edgesInOut()) \/ {e}

hence u1 .edgesInOut() = (u2 .edgesInOut()) \/ {e} by A1, GLIBPRE0:49; :: thesis: verum

end;

end;

end;

{e} misses the_Edges_of G2 by A1, ZFMISC_1:50;
then {e} misses dom g2 by PARTFUN1:def 2;
then A10: g2 | {e} = {} by RELAT_1:66;
A11: g2 | (u1 .edgesInOut()) = (g2 | (u2 .edgesInOut())) \/ (g2 | {e}) by A9, RELAT_1:78
.= g2 | (u2 .edgesInOut()) by A10 ;
not e in u2 .edgesInOut() by A1;
then A12: (e .--> x) | (u2 .edgesInOut()) = {} by FUNCOP_1:76;
A13: (e .--> x) | (u1 .edgesInOut()) = ((e .--> x) | (u2 .edgesInOut())) \/ ((e .--> x) | {e}) by A9, RELAT_1:78
.= e .--> x by A12 ;
rng g2 misses rng (e .--> x) by A2, A4, ZFMISC_1:50;
then A14: rng (g2 | (u2 .edgesInOut())) misses rng (e .--> x) by RELAT_1:70, XBOOLE_1:63;
A15: g2 | (u2 .edgesInOut()) is one-to-one by A2;
g1 | (u1 .edgesInOut()) = (g2 | (u2 .edgesInOut())) +* (e .--> x) by A6, A11, A13;
hence g1 | (u1 .edgesInOut()) is one-to-one by A14, A15, FUNCT_4:92; :: thesis: verum

end;

end;

end;

hence g1 is proper ; :: thesis: verum