let G, G' 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 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 ) ) implies G = G' )
assume that
A25: ( 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 ) ) ) and
A26: ( 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 ) ) ) ; :: thesis: G = G'
A27: ( dom the Source of G = the carrier' of G & dom the Source of G' = the carrier' of G ) by A25, A26, FUNCT_2:def 1;
A28: ( dom the Target of G = the carrier' of G & dom the Target of G' = the carrier' of G ) by A25, A26, FUNCT_2:def 1;
for x being set st x in the carrier' of G holds
the Source of G . x = the Source of G' . x

proof

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

A30: now

assume A31: x in the carrier' of G1 ; :: thesis: the Source of G . x = the Source of G' . x
hence the Source of G . x = the Source of G1 . x by A25
.= the Source of G' . x by A26, A31 ;
:: thesis: verum

end;

now

assume A32: x in the carrier' of G2 ; :: thesis: the Source of G . x = the Source of G' . x
hence the Source of G . x = the Source of G2 . x by A25
.= the Source of G' . x by A26, A32 ;
:: thesis: verum

end;

hence the Source of G . x = the Source of G' . x by A25, A29, A30, XBOOLE_0:def 3; :: thesis: verum

end;

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

proof

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

A35: now

assume A36: x in the carrier' of G1 ; :: thesis: the Target of G . x = the Target of G' . x
hence the Target of G . x = the Target of G1 . x by A25
.= the Target of G' . x by A26, A36 ;
:: thesis: verum

end;

now

assume A37: x in the carrier' of G2 ; :: thesis: the Target of G . x = the Target of G' . x
hence the Target of G . x = the Target of G2 . x by A25
.= the Target of G' . x by A26, A37 ;
:: thesis: verum

end;

hence the Target of G . x = the Target of G' . x by A25, A34, A35, XBOOLE_0:def 3; :: thesis: verum

end;

hence G = G' by A25, A26, A28, A33, FUNCT_1:9; :: thesis: verum