let G, G9 be strict Graph; :: thesis: ( the carrier of G = the carrier of G1 \/ the carrier of G2 & the carrier' of G = the carrier' of G1 \/ the carrier' of G2 & ( for v being set st v in the carrier' of G1 holds
( the Source of G . v = the Source of G1 . v & the Target of G . v = the Target of G1 . v ) ) & ( for v being set st v in the carrier' of G2 holds
( the Source of G . v = the Source of G2 . v & the Target of G . v = the Target of G2 . v ) ) & the carrier of G9 = the carrier of G1 \/ the carrier of G2 & the carrier' of G9 = the carrier' of G1 \/ the carrier' of G2 & ( for v being set st v in the carrier' of G1 holds
( the Source of G9 . v = the Source of G1 . v & the Target of G9 . v = the Target of G1 . v ) ) & ( for v being set st v in the carrier' of G2 holds
( the Source of G9 . v = the Source of G2 . v & the Target of G9 . v = the Target of G2 . v ) ) implies G = G9 )
assume that
A46: the carrier of G = the carrier of G1 \/ the carrier of G2 and
A47: the carrier' of G = the carrier' of G1 \/ the carrier' of G2 and
A48: for v being set st v in the carrier' of G1 holds
( the Source of G . v = the Source of G1 . v & the Target of G . v = the Target of G1 . v ) and
A49: for v being set st v in the carrier' of G2 holds
( the Source of G . v = the Source of G2 . v & the Target of G . v = the Target of G2 . v ) and
A50: the carrier of G9 = the carrier of G1 \/ the carrier of G2 and
A51: the carrier' of G9 = the carrier' of G1 \/ the carrier' of G2 and
A52: for v being set st v in the carrier' of G1 holds
( the Source of G9 . v = the Source of G1 . v & the Target of G9 . v = the Target of G1 . v ) and
A53: for v being set st v in the carrier' of G2 holds
( the Source of G9 . v = the Source of G2 . v & the Target of G9 . v = the Target of G2 . v ) ; :: thesis: G = G9
A54: ( dom the Source of G = the carrier' of G & dom the Source of G9 = the carrier' of G ) by A47, A51, FUNCT_2:def 1;
A55: ( dom the Target of G = the carrier' of G & dom the Target of G9 = the carrier' of G ) by A47, A51, FUNCT_2:def 1;
for x being set st x in the carrier' of G holds
the Source of G . x = the Source of G9 . x

proof

let x be set ; :: thesis: ( x in the carrier' of G implies the Source of G . x = the Source of G9 . x )
assume A57: x in the carrier' of G ; :: thesis: the Source of G . x = the Source of G9 . x

A58: now

assume A59: x in the carrier' of G1 ; :: thesis: the Source of G . x = the Source of G9 . x
hence the Source of G . x = the Source of G1 . x by A48
.= the Source of G9 . x by A52, A59 ;
:: thesis: verum

end;

now

assume A61: x in the carrier' of G2 ; :: thesis: the Source of G . x = the Source of G9 . x
hence the Source of G . x = the Source of G2 . x by A49
.= the Source of G9 . x by A53, A61 ;
:: thesis: verum

end;

hence the Source of G . x = the Source of G9 . x by A47, A57, A58, XBOOLE_0:def 3; :: thesis: verum

end;

then A62: the Source of G = the Source of G9 by A54, FUNCT_1:9;
for x being set st x in the carrier' of G holds
the Target of G . x = the Target of G9 . x

proof

let x be set ; :: thesis: ( x in the carrier' of G implies the Target of G . x = the Target of G9 . x )
assume A64: x in the carrier' of G ; :: thesis: the Target of G . x = the Target of G9 . x

A65: now

assume A66: x in the carrier' of G1 ; :: thesis: the Target of G . x = the Target of G9 . x
hence the Target of G . x = the Target of G1 . x by A48
.= the Target of G9 . x by A52, A66 ;
:: thesis: verum

end;

now

assume A68: x in the carrier' of G2 ; :: thesis: the Target of G . x = the Target of G9 . x
hence the Target of G . x = the Target of G2 . x by A49
.= the Target of G9 . x by A53, A68 ;
:: thesis: verum

end;

hence the Target of G . x = the Target of G9 . x by A47, A64, A65, XBOOLE_0:def 3; :: thesis: verum

end;

hence G = G9 by A46, A47, A50, A51, A55, A62, FUNCT_1:9; :: thesis: verum