let G1, G3, G2, G be Graph; :: thesis: ( 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 ; :: thesis: G c= G3
A4: ( the Source of G1 tolerates the Source of G2 & the Target of G1 tolerates the Target of G2 ) by A3, Def4;
A5: MultiGraphStruct(# the carrier of G,the carrier' of G,the Source of G,the Target of G #) = G1 \/ G2 by A3, Def4;
A6: G1 is Subgraph of G3 by A1, Def24;
A7: G2 is Subgraph of G3 by A2, Def24;
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 A10: the carrier of G1 \/ the carrier of G2 c= the carrier of G3 by A8, XBOOLE_1:8;
A11: 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 A13: the carrier' of G1 \/ the carrier' of G2 c= the carrier' of G3 by A11, 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) )

proof

let v be set ; :: thesis: ( v in the carrier' of (G1 \/ G2) implies ( 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) ) )
assume A15: v in the carrier' of (G1 \/ G2) ; :: thesis: ( 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) )
thus A16: ( the Source of (G1 \/ G2) . v = the Source of G3 . v & the Target of (G1 \/ G2) . v = the Target of G3 . v ) :: thesis: ( the Source of G3 . v in the carrier of (G1 \/ G2) & the Target of G3 . v in the carrier of (G1 \/ G2) )

proof

A17: v in the carrier' of G1 \/ the carrier' of G2 by A4, A15, Def3;

A18: now

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

end;

now

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

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 A17, A18, XBOOLE_0:def 3; :: thesis: verum

end;

hence the Source of G3 . v in the carrier of (G1 \/ G2) by A15, FUNCT_2:7; :: thesis: the Target of G3 . v in the carrier of (G1 \/ G2)
thus the Target of G3 . v in the carrier of (G1 \/ G2) by A15, A16, FUNCT_2:7; :: thesis: verum

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