let G, G1, G2, G3 be Graph; :: thesis:
assume that
A1: G1 c= G3 and
A2: G2 c= G3 and
A3: G is_sum_of G1,G2 ; :: thesis:
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) )

let v be set ; :: thesis:
assume A12: v in the carrier' of (G1 \/ G2) ; :: thesis:
thus A13: ( the Source of (G1 \/ G2) . v = the Source of G3 . v & the Target of (G1 \/ G2) . v = the Target of G3 . v ) :: thesis:

A14: v in the carrier' of G1 \/ the carrier' of G2 by A4, A12, Def5;

assume A16: v in the carrier' of G1 ; :: thesis:
then A17: the Source of G3 . v = the Source of G1 . v by A6, Def18
.= the Source of (G1 \/ G2) . v by A4, A16, Def5 ;
the Target of G3 . v = the Target of G1 . v by A6, A16, Def18
.= the Target of (G1 \/ G2) . v by A4, A16, Def5 ;
hence ( the Source of (G1 \/ G2) . v = the Source of G3 . v & the Target of (G1 \/ G2) . v = the Target of G3 . v ) by A17; :: thesis:

end;

assume A18: v in the carrier' of G2 ; :: thesis:
then A19: the Source of G3 . v = the Source of G2 . v by A7, Def18
.= the Source of (G1 \/ G2) . v by A4, A18, Def5 ;
the Target of G3 . v = the Target of G2 . v by A7, A18, Def18
.= the Target of (G1 \/ G2) . v by A4, A18, Def5 ;
hence ( the Source of (G1 \/ G2) . v = the Source of G3 . v & the Target of (G1 \/ G2) . v = the Target of G3 . v ) by A19; :: thesis:

end;

hence ( the Source of (G1 \/ G2) . v = the Source of G3 . v & the Target of (G1 \/ G2) . v = the Target of G3 . v ) by A14, A15, XBOOLE_0:def 3; :: thesis:

end;

end;

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; :: according to GRAPH_1:def 18,GRAPH_1:def 24 :: thesis: