let G be _Graph; :: thesis: for g being EColoring of G
for H being Subgraph of G holds g | (the_Edges_of H) is EColoring of H
let g be EColoring of G; :: thesis: for H being Subgraph of G holds g | (the_Edges_of H) is EColoring of H
let H be Subgraph of G; :: thesis: g | (the_Edges_of H) is EColoring of H
set g9 = g | (the_Edges_of H);
the_Edges_of H c= the_Edges_of G ;
then the_Edges_of H c= dom g by PARTFUN1:def 2;
then dom (g | (the_Edges_of H)) = the_Edges_of H by RELAT_1:62;
hence g | (the_Edges_of H) is EColoring of H by PARTFUN1:def 2; :: thesis: verum