let G1, G2 be _Graph; :: thesis: for S being GraphSum of G1,G2 holds S .size() = (G1 .size()) +` (G2 .size())
let S be GraphSum of G1,G2; :: thesis: S .size() = (G1 .size()) +` (G2 .size())
S is GraphSum of <*G1,G2*> by Def28;
then consider G9 being GraphUnion of rng (canGFDistinction <*G1,G2*>) 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;
consider G3, G4 being _Graph such that
A3: the_Edges_of G3 misses the_Edges_of G4 and
A4: G3 tolerates G4 and
the_Vertices_of G3 misses the_Vertices_of G4 and
A5: G9 is GraphUnion of G3,G4 and
A6: ( G3 is G1 -Disomorphic & G4 is G2 -Disomorphic ) by Lm6;
consider H1 being PGraphMapping of G1,G3 such that
A7: H1 is Disomorphism by A6, GLIB_010:def 24;
consider H2 being PGraphMapping of G2,G4 such that
A8: H2 is Disomorphism by A6, GLIB_010:def 24;
thus S .size() = G9 .size() by A2, GLIB_010:84
.= (G3 .size()) +` (G4 .size()) by A3, A4, A5, GLIBPRE1:121
.= (G1 .size()) +` (G4 .size()) by A7, GLIB_010:84
.= (G1 .size()) +` (G2 .size()) by A8, GLIB_010:84 ; :: thesis: verum