ex f being Function st
( G . ELabelSelector = f & dom f c= the_Edges_of G ) by Def5;
hence G . ELabelSelector is Function ; :: thesis: verum