let G be _Graph; :: thesis: ( G is finite-ecolorable implies G is locally-finite )
assume A2: G is finite-ecolorable ; :: thesis: G is locally-finite

now :: thesis: for v being Vertex of G holds v .edgesInOut() is finite

let v be Vertex of G; :: thesis: v .edgesInOut() is finite
consider n being Nat such that
A3: G is n -ecolorable by A2;
consider g being proper EColoring of G such that
A4: card (rng g) c= n by A3;
A5: g | (v .edgesInOut()) is one-to-one by Def5;
rng (g | (v .edgesInOut())) c= rng g by RELAT_1:70;
then card (rng (g | (v .edgesInOut()))) c= card (rng g) by CARD_1:11;
then rng (g | (v .edgesInOut())) is finite by A4;
then A6: dom (g | (v .edgesInOut())) is finite by A5, CARD_1:59;
dom (g | (v .edgesInOut())) = (dom g) /\ (v .edgesInOut()) by RELAT_1:61
.= (the_Edges_of G) /\ (v .edgesInOut()) by PARTFUN1:def 2
.= v .edgesInOut() by XBOOLE_1:28 ;
hence v .edgesInOut() is finite by A6; :: thesis: verum

end;

hence G is locally-finite by GLIB_013:def 5; :: thesis: verum