theorem :: GLIB_015:102

for F being non empty Graph-yielding Function
for z being Element of dom F holds the_Edges_of (canGFDistinction (F,z)) = (the_Edges_of (canGFDistinction F)) +* (z,(the_Edges_of (F . z)))