let G be _Graph; :: according to GLPACY00:def 10 :: thesis: ( G in rng F implies G is Cycle-like )
assume G in rng F ; :: thesis: G is Cycle-like
then consider x being object such that
A1: ( x in dom F & F . x = G ) by FUNCT_1:def 3;
consider G0 being _Graph such that
A2: ( F . x = G0 & G0 is Cycle-like ) by A1, Def7;
thus G is Cycle-like by A1, A2; :: thesis: verum