let F be non empty Graph-yielding Function; :: thesis:
let S be GraphSum of F; :: thesis:
consider G9 being GraphUnion of rng (canGFDistinction F) such that
A1: S is G9 -Disomorphic by Def27;
consider H being PGraphMapping of G9,S such that
A2: H is Disomorphism by A1, GLIB_010:def 24;
F, canGFDistinction F are_Disomorphic by Th87;
then A3: F, canGFDistinction F are_isomorphic by Th42;
thus ( F is acyclic implies S is acyclic ) by A2, GLIB_010:140; :: thesis:

hereby :: thesis:

assume S is acyclic ; :: thesis:
then G9 is acyclic by A2, GLIB_010:140;
then rng (canGFDistinction F) is acyclic by Th60;
hence F is acyclic by GLIB_014:3; :: thesis:

end;

hereby :: thesis:

assume F is chordal ; :: thesis:
then canGFDistinction F is chordal by A3, Th48;
then G9 is chordal by Th63;
hence S is chordal by A2, GLIB_010:140; :: thesis:

end;

hereby :: thesis:

assume S is chordal ; :: thesis:
then G9 is chordal by A2, GLIB_010:140;
then rng (canGFDistinction F) is chordal by Th63;
then canGFDistinction F is chordal by GLIB_014:3;
hence F is chordal by A3, Th48; :: thesis:

end;