theorem :: GLIB_010:14

for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 holds
( F is directed iff ( (the_Source_of G2) * (F _E) = (F _V) * ((the_Source_of G1) | (dom (F _E))) & (the_Target_of G2) * (F _E) = (F _V) * ((the_Target_of G1) | (dom (F _E))) ) )