let G be _Graph; :: thesis: for g being EColoring of G
for g9 being Function st rng g c= dom g9 holds
g9 * g is EColoring of G
let g be EColoring of G; :: thesis: for g9 being Function st rng g c= dom g9 holds
g9 * g is EColoring of G
let g9 be Function; :: thesis: ( rng g c= dom g9 implies g9 * g is EColoring of G )
assume rng g c= dom g9 ; :: thesis: g9 * g is EColoring of G
then dom (g9 * g) = dom g by RELAT_1:27
.= the_Edges_of G by PARTFUN1:def 2 ;
hence g9 * g is EColoring of G by PARTFUN1:def 2; :: thesis: verum