let G1, G2 be _Graph; :: thesis: for S being GraphSum of G1,G2 holds S .order() = (G1 .order()) +` (G2 .order())
let S be GraphSum of G1,G2; :: thesis: S .order() = (G1 .order()) +` (G2 .order())
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
the_Edges_of G3 misses the_Edges_of G4 and
A3: G3 tolerates G4 and
A4: 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 .order() = G9 .order() by A2, GLIB_010:84
.= (G3 .order()) +` (G4 .order()) by A3, A4, A5, GLIBPRE1:120
.= (G1 .order()) +` (G4 .order()) by A7, GLIB_010:84
.= (G1 .order()) +` (G2 .order()) by A8, GLIB_010:84 ; :: thesis: verum