theorem :: GLIB_015:27

for F being Graph-yielding Function holds the_Target_of (rng F) = rng (the_Target_of F)