let G2 be _Graph; :: thesis: ( G2 is G -isomorphic implies G2 is finite-ecolorable )
assume G2 is G -isomorphic ; :: thesis: G2 is finite-ecolorable
then consider F being PGraphMapping of G,G2 such that
A1: F is isomorphism by GLIB_010:def 23;
thus G2 is finite-ecolorable by A1, Th119; :: thesis: verum