set G = the _Graph;
set F = NAT --> the _Graph;
A1: dom (NAT --> the _Graph) = NAT by FUNCOP_1:13;
reconsider F = NAT --> the _Graph as ManySortedSet of NAT ;
take F ; :: thesis: F is Graph-yielding
let x be Nat; :: according to GLIB_000:def 53 :: thesis: F . x is _Graph
x in NAT by ORDINAL1:def 12;
then F . x in rng F by A1, FUNCT_1:3;
then F . x in { the _Graph} by FUNCOP_1:8;
hence F . x is _Graph by TARSKI:def 1; :: thesis: verum