let G, G1 be _Graph; :: thesis: for g being EColoring of G
for F being PGraphMapping of G1,G st F is total holds
g * (F _E) is EColoring of G1
let g be EColoring of G; :: thesis: for F being PGraphMapping of G1,G st F is total holds
g * (F _E) is EColoring of G1
let F be PGraphMapping of G1,G; :: thesis: ( F is total implies g * (F _E) is EColoring of G1 )
assume F is total ; :: thesis: g * (F _E) is EColoring of G1
then dom (F _E) = the_Edges_of G1 by GLIB_010:def 11;
hence g * (F _E) is EColoring of G1 by Th83; :: thesis: verum