let G, G1 be _Graph; :: thesis: for g being EColoring of G
for F being PGraphMapping of G1,G
for g9 being EColoring of G1 st dom (F _E) = the_Edges_of G1 & F _E is one-to-one & g9 = g * (F _E) & g is proper holds
g9 is proper
let g be EColoring of G; :: thesis: for F being PGraphMapping of G1,G
for g9 being EColoring of G1 st dom (F _E) = the_Edges_of G1 & F _E is one-to-one & g9 = g * (F _E) & g is proper holds
g9 is proper
let F be PGraphMapping of G1,G; :: thesis: for g9 being EColoring of G1 st dom (F _E) = the_Edges_of G1 & F _E is one-to-one & g9 = g * (F _E) & g is proper holds
g9 is proper
let g9 be EColoring of G1; :: thesis: ( dom (F _E) = the_Edges_of G1 & F _E is one-to-one & g9 = g * (F _E) & g is proper implies g9 is proper )
assume A1: ( dom (F _E) = the_Edges_of G1 & F _E is one-to-one & g9 = g * (F _E) & g is proper ) ; :: thesis: g9 is proper

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

let v be Vertex of G1; :: thesis: for e1, e2 being object st e1 in v .edgesInOut() & e2 in v .edgesInOut() & g9 . e1 = g9 . e2 holds
e1 = e2
let e1, e2 be object ; :: thesis: ( e1 in v .edgesInOut() & e2 in v .edgesInOut() & g9 . e1 = g9 . e2 implies e1 = e2 )
assume A2: ( e1 in v .edgesInOut() & e2 in v .edgesInOut() & g9 . e1 = g9 . e2 ) ; :: thesis: e1 = e2
then A3: ( g9 . e1 = g . ((F _E) . e1) & g9 . e2 = g . ((F _E) . e2) ) by A1, FUNCT_1:13;
( (the_Source_of G1) . e1 = v or (the_Target_of G1) . e1 = v ) by A2, GLIB_000:61;
then v in dom (F _V) by A1, A2, GLIB_010:5;
then A4: (F _E) .: (v .edgesInOut()) c= ((F _V) /. v) .edgesInOut() by GLIBPRE0:80;
( (F _E) . e1 in (F _E) .: (v .edgesInOut()) & (F _E) . e2 in (F _E) .: (v .edgesInOut()) ) by A1, A2, FUNCT_1:def 6;
then ( (F _E) . e1 in ((F _V) /. v) .edgesInOut() & (F _E) . e2 in ((F _V) /. v) .edgesInOut() ) by A4;
then (F _E) . e1 = (F _E) . e2 by A1, A2, A3, Th85;
hence e1 = e2 by A1, A2, FUNCT_1:def 4; :: thesis: verum

end;

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