let G be _Graph; :: thesis: for f being VColoring of G
for H being Subgraph of G holds f | (the_Vertices_of H) is VColoring of H
let f be VColoring of G; :: thesis: for H being Subgraph of G holds f | (the_Vertices_of H) is VColoring of H
let H be Subgraph of G; :: thesis: f | (the_Vertices_of H) is VColoring of H
set f9 = f | (the_Vertices_of H);
the_Vertices_of H c= the_Vertices_of G ;
then the_Vertices_of H c= dom f by PARTFUN1:def 2;
then dom (f | (the_Vertices_of H)) = the_Vertices_of H by RELAT_1:62;
hence f | (the_Vertices_of H) is VColoring of H by PARTFUN1:def 2; :: thesis: verum