thus not SG2SGFunc F is empty ; :: thesis: SG2SGFunc F is Graph-yielding

now :: thesis: for x being object st x in dom (SG2SGFunc F) holds
(SG2SGFunc F) . x is _Graph

let x be object ; :: thesis: ( x in dom (SG2SGFunc F) implies (SG2SGFunc F) . x is _Graph )
assume x in dom (SG2SGFunc F) ; :: thesis: (SG2SGFunc F) . x is _Graph
then reconsider H = x as plain Subgraph of G1 by Th1;
(SG2SGFunc F) . H = rng (F | H) by Def5;
hence (SG2SGFunc F) . x is _Graph ; :: thesis: verum

end;

hence SG2SGFunc F is Graph-yielding by GLIB_000:def 53; :: thesis: verum