per cases ( X <> {} or X = {} ) ;
suppose A1: X <> {} ; :: thesis: X --> G is Graph-yielding
set F = X --> G;
reconsider F = X --> G as ManySortedSet of X ;
now :: thesis: for x being object st x in dom F holds
F . x is _Graph
let x be object ; :: thesis: ( x in dom F implies F . x is _Graph )
assume x in dom F ; :: thesis: F . x is _Graph
then F . x in rng F by FUNCT_1:3;
then F . x in {G} by A1, FUNCOP_1:8;
hence F . x is _Graph ; :: thesis: verum
end;
hence X --> G is Graph-yielding by GLIB_000:def 53; :: thesis: verum
end;
suppose X = {} ; :: thesis: X --> G is Graph-yielding
hence X --> G is Graph-yielding ; :: thesis: verum
end;
end;