let F be non empty Graph-yielding Function; 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; 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)); 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 ; ( z = z9 implies ( e DJoins v,w,F . z iff e DJoins v,w,(canGFDistinction (F,z)) . z9 ) )
assume A1:
z = z9
; ( e DJoins v,w,F . z iff e DJoins v,w,(canGFDistinction (F,z)) . z9 )
F . z == (F . z) | _GraphSelectors
by GLIB_009:9;
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; verum