now :: thesis: for x being object st x in dom ((canGFDistinction F) +* (z,((F . z) | _GraphSelectors))) holds
((canGFDistinction F) +* (z,((F . z) | _GraphSelectors))) . x is _Graph

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

per cases ( x = z or x <> z ) ;

suppose x = z ; :: thesis: ((canGFDistinction F) +* (z,((F . z) | _GraphSelectors))) . b₁ is _Graph

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

end;

suppose x <> z ; :: thesis: ((canGFDistinction F) +* (z,((F . z) | _GraphSelectors))) . b₁ is _Graph

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: verum

end;

end;

end;

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