let x be object ; :: thesis:
assume x in dom ((canGFDistinction F) +* (z,((F . z) | _GraphSelectors))) ; :: thesis:
then A1: x in dom (canGFDistinction F) by FUNCT_7:30;
z in dom F ;
then A2: z in dom (canGFDistinction F) by Def25;

suppose x = z ; :: thesis:

hence ((canGFDistinction F) +* (z,((F . z) | _GraphSelectors))) . x is _Graph by A2, FUNCT_7:31; :: thesis:

end;

suppose x <> z ; :: thesis:

then ((canGFDistinction F) +* (z,((F . z) | _GraphSelectors))) . x = (canGFDistinction F) . x by FUNCT_7:32;
hence ((canGFDistinction F) +* (z,((F . z) | _GraphSelectors))) . x is _Graph by A1; :: thesis:

end;

end;

end;

hence (canGFDistinction F) +* (z,((F . z) | _GraphSelectors)) is Graph-yielding Function by GLIB_000:def 53; :: thesis: