let G be _Graph; :: thesis: for g being EColoring of G holds
( g is proper iff for v being Vertex of G
for e1, e2 being object st e1 in v .edgesInOut() & e2 in v .edgesInOut() & g . e1 = g . e2 holds
e1 = e2 )
let g be EColoring of G; :: thesis: ( g is proper iff for v being Vertex of G
for e1, e2 being object st e1 in v .edgesInOut() & e2 in v .edgesInOut() & g . e1 = g . e2 holds
e1 = e2 )

hereby :: thesis: ( ( for v being Vertex of G
for e1, e2 being object st e1 in v .edgesInOut() & e2 in v .edgesInOut() & g . e1 = g . e2 holds
e1 = e2 ) implies g is proper )

assume A1: g is proper ; :: thesis: for v being Vertex of G
for e1, e2 being object st e1 in v .edgesInOut() & e2 in v .edgesInOut() & g . e1 = g . e2 holds
e1 = e2
let v be Vertex of G; :: thesis: for e1, e2 being object st e1 in v .edgesInOut() & e2 in v .edgesInOut() & g . e1 = g . e2 holds
e1 = e2
let e1, e2 be object ; :: thesis: ( e1 in v .edgesInOut() & e2 in v .edgesInOut() & g . e1 = g . e2 implies e1 = e2 )
set V = v .edgesInOut() ;
assume A2: ( e1 in v .edgesInOut() & e2 in v .edgesInOut() & g . e1 = g . e2 ) ; :: thesis: e1 = e2
v .edgesInOut() c= the_Edges_of G ;
then v .edgesInOut() c= dom g by PARTFUN1:def 2;
then A3: ( e1 in dom (g | (v .edgesInOut())) & e2 in dom (g | (v .edgesInOut())) ) by A2, RELAT_1:62;
then ( g . e1 = (g | (v .edgesInOut())) . e1 & g . e2 = (g | (v .edgesInOut())) . e2 ) by FUNCT_1:47;
then ( (g | (v .edgesInOut())) . e1 = (g | (v .edgesInOut())) . e2 & g | (v .edgesInOut()) is one-to-one ) by A1, A2;
hence e1 = e2 by A3, FUNCT_1:def 4; :: thesis: verum

end;

assume A4: for v being Vertex of G
for e1, e2 being object st e1 in v .edgesInOut() & e2 in v .edgesInOut() & g . e1 = g . e2 holds
e1 = e2 ; :: thesis: g is proper
let v be Vertex of G; :: according to GLCOLO00:def 5 :: thesis: g | (v .edgesInOut()) is one-to-one
set V = v .edgesInOut() ;

now :: thesis: for e1, e2 being object st e1 in dom (g | (v .edgesInOut())) & e2 in dom (g | (v .edgesInOut())) & (g | (v .edgesInOut())) . e1 = (g | (v .edgesInOut())) . e2 holds
e1 = e2

let e1, e2 be object ; :: thesis: ( e1 in dom (g | (v .edgesInOut())) & e2 in dom (g | (v .edgesInOut())) & (g | (v .edgesInOut())) . e1 = (g | (v .edgesInOut())) . e2 implies e1 = e2 )
assume A5: ( e1 in dom (g | (v .edgesInOut())) & e2 in dom (g | (v .edgesInOut())) & (g | (v .edgesInOut())) . e1 = (g | (v .edgesInOut())) . e2 ) ; :: thesis: e1 = e2
then ( g . e1 = (g | (v .edgesInOut())) . e1 & g . e2 = (g | (v .edgesInOut())) . e2 ) by FUNCT_1:47;
hence e1 = e2 by A5, A4; :: thesis: verum

end;

hence g | (v .edgesInOut()) is one-to-one by FUNCT_1:def 4; :: thesis: verum