set F = NAT --> G;
A1: dom (NAT --> G) = NAT ;
reconsider F = NAT --> G as ManySortedSet of NAT ;
let x be Nat; :: according to GLIB_000:def 54 :: thesis: (NAT --> G) . 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 {G} by FUNCOP_1:8;
hence (NAT --> G) . x is _Graph by TARSKI:def 1; :: thesis: verum