let G, G9 be strict Graph; ( 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
A28:
the carrier of G = the carrier of G1 \/ the carrier of G2
and
A29:
the carrier' of G = the carrier' of G1 \/ the carrier' of G2
and
A30:
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
A31:
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
A32:
the carrier of G9 = the carrier of G1 \/ the carrier of G2
and
A33:
the carrier' of G9 = the carrier' of G1 \/ the carrier' of G2
and
A34:
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
A35:
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 )
; G = G9
A36:
( dom the Source of G = the carrier' of G & dom the Source of G9 = the carrier' of G )
by A29, A33, FUNCT_2:def 1;
A37:
( dom the Target of G = the carrier' of G & dom the Target of G9 = the carrier' of G )
by A29, A33, FUNCT_2:def 1;
for x being object st x in the carrier' of G holds
the Source of G . x = the Source of G9 . x
then A42:
the Source of G = the Source of G9
by A36;
for x being object st x in the carrier' of G holds
the Target of G . x = the Target of G9 . x
hence
G = G9
by A28, A29, A32, A33, A37, A42, FUNCT_1:2; verum