let y be object ; :: according to GLIB_014:def 1 :: thesis: ( y in rng F implies y is _Graph )
assume y in rng F ; :: thesis: y is _Graph
then consider x being object such that
A1: ( x in dom F & F . x = y ) by FUNCT_1:def 3;
thus y is _Graph by A1, GLIB_000:def 53; :: thesis: verum