:: deftheorem defines dom GLIB_010:def 29 :
for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 holds dom F = the plain inducedSubgraph of G1, dom (F _V), dom (F _E);