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 by TARSKI:def 1; :: thesis: verum

end;

hence X --> G is Graph-yielding ; :: thesis: verum

end;

suppose X = {} ; :: thesis: X --> G is Graph-yielding

hence X --> G is Graph-yielding ; :: thesis: verum

end;

end;