1 in {1,2} by TARSKI:def 2;
then reconsider z = 1 as Element of dom <*G1,G2*> by FINSEQ_1:92;
consider S being GraphSum of <*G1,G2*> such that
A1: S is Supergraph of <*G1,G2*> . z and
S is GraphUnion of rng (canGFDistinction (<*G1,G2*>,z)) by Th123;
reconsider S = S as Supergraph of G1 by A1, FINSEQ_1:44;
take S ; :: thesis: S is GraphSum of <*G1,G2*>
thus S is GraphSum of <*G1,G2*> ; :: thesis: verum