let F be Function; :: thesis: ( F is empty implies F is Graph-yielding )
assume F is empty ; :: thesis: F is Graph-yielding
then for x being object st x in dom F holds
F . x is _Graph ;
hence F is Graph-yielding by Def53; :: thesis: verum