x .--> G = {x} --> G by FUNCOP_1:def 9;
hence x .--> G is Graph-yielding ; :: thesis: verum