let G, G1 be _Graph; :: thesis: for g being EColoring of G
for F being PGraphMapping of G1,G st dom (F _E) = the_Edges_of G1 holds
g * (F _E) is EColoring of G1
let g be EColoring of G; :: thesis: for F being PGraphMapping of G1,G st dom (F _E) = the_Edges_of G1 holds
g * (F _E) is EColoring of G1
let F be PGraphMapping of G1,G; :: thesis: ( dom (F _E) = the_Edges_of G1 implies g * (F _E) is EColoring of G1 )
assume A1: dom (F _E) = the_Edges_of G1 ; :: thesis: g * (F _E) is EColoring of G1
rng (F _E) c= the_Edges_of G ;
then rng (F _E) c= dom g by PARTFUN1:def 2;
then dom (g * (F _E)) = dom (F _E) by RELAT_1:27;
hence g * (F _E) is EColoring of G1 by A1, PARTFUN1:def 2; :: thesis: verum