let F be non empty Graph-yielding Function; :: thesis: for z being Element of dom F ex S being GraphSum of F st
( S is Supergraph of F . z & S is GraphUnion of rng (canGFDistinction (F,z)) )
let z be Element of dom F; :: thesis: ex S being GraphSum of F st
( S is Supergraph of F . z & S is GraphUnion of rng (canGFDistinction (F,z)) )
set S = the GraphUnion of rng (canGFDistinction (F,z));
set G9 = the GraphUnion of rng (canGFDistinction F);
set G0 = (F . z) | _GraphSelectors;
canGFDistinction F, canGFDistinction (F,z) are_Disomorphic by Th106;
then the GraphUnion of rng (canGFDistinction (F,z)) is the GraphUnion of rng (canGFDistinction F) -Disomorphic by Th55, Th74;
then reconsider S = the GraphUnion of rng (canGFDistinction (F,z)) as GraphSum of F by Def27;
take S ; :: thesis: ( S is Supergraph of F . z & S is GraphUnion of rng (canGFDistinction (F,z)) )
z in dom F ;
then z in dom (canGFDistinction (F,z)) by Th94;
then (canGFDistinction (F,z)) . z in rng (canGFDistinction (F,z)) by FUNCT_1:3;
then (F . z) | _GraphSelectors in rng (canGFDistinction (F,z)) by Th95;
then A1: (F . z) | _GraphSelectors is Subgraph of S by GLIB_014:21;
(F . z) | _GraphSelectors == F . z by GLIB_000:128;
then F . z is Subgraph of S by A1, GLIB_000:92;
hence ( S is Supergraph of F . z & S is GraphUnion of rng (canGFDistinction (F,z)) ) by GLIB_006:57; :: thesis: verum