let F be non empty Graph-yielding Function; :: thesis: for S being GraphSum of F holds card F c= S .numComponents()
let S be GraphSum of F; :: thesis: card F c= S .numComponents()
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;
A3: card F = card (dom F) by CARD_1:62
.= card (dom (canGFDistinction F)) by Def25
.= card (rng (canGFDistinction F)) by CARD_1:70 ;
S .numComponents() = G9 .numComponents() by A2, GLIBPRE1:83;
hence card F c= S .numComponents() by A3, Th68; :: thesis: verum