let F be non empty Graph-yielding Function; :: thesis: for z being Element of dom F
for z9 being Element of dom (canGFDistinction (F,z))
for v, e, w being object st z = z9 holds
( e DJoins v,w,F . z iff e DJoins v,w,(canGFDistinction (F,z)) . z9 )
let z be Element of dom F; :: thesis: for z9 being Element of dom (canGFDistinction (F,z))
for v, e, w being object st z = z9 holds
( e DJoins v,w,F . z iff e DJoins v,w,(canGFDistinction (F,z)) . z9 )
let z9 be Element of dom (canGFDistinction (F,z)); :: thesis: for v, e, w being object st z = z9 holds
( e DJoins v,w,F . z iff e DJoins v,w,(canGFDistinction (F,z)) . z9 )
let v, e, w be object ; :: thesis: ( z = z9 implies ( e DJoins v,w,F . z iff e DJoins v,w,(canGFDistinction (F,z)) . z9 ) )
assume A1: z = z9 ; :: thesis: ( e DJoins v,w,F . z iff e DJoins v,w,(canGFDistinction (F,z)) . z9 )
F . z == (F . z) | _GraphSelectors by GLIB_000:128;
then F . z == (canGFDistinction (F,z)) . z9 by A1, Th96;
hence ( e DJoins v,w,F . z iff e DJoins v,w,(canGFDistinction (F,z)) . z9 ) by GLIB_000:88; :: thesis: verum