theorem :: GLIB_015:26

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