let F be non empty Graph-yielding Function; :: thesis: for S being GraphSum of F st S is connected holds
ex x being object ex G being connected _Graph st F = x .--> G
let S be GraphSum of F; :: thesis: ( S is connected implies ex x being object ex G being connected _Graph st F = x .--> G )
assume A1: S is connected ; :: thesis: ex x being object ex G being connected _Graph st F = x .--> G
consider G9 being GraphUnion of rng (canGFDistinction F) such that
A2: S is G9 -Disomorphic by Def27;
consider M being PGraphMapping of G9,S such that
A3: M is Disomorphism by A2, GLIB_010:def 24;
G9 is connected by A1, A3, GLIB_010:140;
then consider H being _Graph such that
A4: rng (canGFDistinction F) = {H} by Th59;
consider x being object such that
A5: canGFDistinction F = x .--> H by A4, GLIBPRE1:4;
A6: {x} = dom {[x,H]} by RELAT_1:9
.= dom (canGFDistinction F) by A5, FUNCT_4:82
.= dom F by Def25 ;
then reconsider x0 = x as Element of dom F by TARSKI:def 1;
A7: F = x .--> (F . x0) by A6, DICKSON:1;
then S is F . x0 -Disomorphic by Th120;
then consider M being PGraphMapping of F . x0,S such that
A8: M is Disomorphism by GLIB_010:def 24;
reconsider G = F . x0 as connected _Graph by A1, A8, GLIB_010:140;
take x ; :: thesis: ex G being connected _Graph st F = x .--> G
take G ; :: thesis: F = x .--> G
thus F = x .--> G by A7; :: thesis: verum