let G, G1, G2, G3 be Graph; ( G1 c= G3 & G2 c= G3 & G is_sum_of G1,G2 implies G c= G3 )
assume that
A1:
G1 c= G3
and
A2:
G2 c= G3
and
A3:
G is_sum_of G1,G2
; G c= G3
A4:
( the Source of G1 tolerates the Source of G2 & the Target of G1 tolerates the Target of G2 )
by A3;
A5:
MultiGraphStruct(# the carrier of G, the carrier' of G, the Source of G, the Target of G #) = G1 \/ G2
by A3;
A6:
G1 is Subgraph of G3
by A1;
A7:
G2 is Subgraph of G3
by A2;
A8:
the carrier of G1 c= the carrier of G3
by A6, Def18;
the carrier of G2 c= the carrier of G3
by A7, Def18;
then A9:
the carrier of G1 \/ the carrier of G2 c= the carrier of G3
by A8, XBOOLE_1:8;
A10:
the carrier' of G1 c= the carrier' of G3
by A6, Def18;
the carrier' of G2 c= the carrier' of G3
by A7, Def18;
then A11:
the carrier' of G1 \/ the carrier' of G2 c= the carrier' of G3
by A10, XBOOLE_1:8;
for v being set st v in the carrier' of (G1 \/ G2) holds
( the Source of (G1 \/ G2) . v = the Source of G3 . v & the Target of (G1 \/ G2) . v = the Target of G3 . v & the Source of G3 . v in the carrier of (G1 \/ G2) & the Target of G3 . v in the carrier of (G1 \/ G2) )
hence
( the carrier of G c= the carrier of G3 & the carrier' of G c= the carrier' of G3 & ( for v being set st v in the carrier' of G holds
( the Source of G . v = the Source of G3 . v & the Target of G . v = the Target of G3 . v & the Source of G3 . v in the carrier of G & the Target of G3 . v in the carrier of G ) ) )
by A4, A5, A9, A11, Def5; GRAPH_1:def 18,GRAPH_1:def 24 verum