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
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 ) ; :: thesis: 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
proof
let x be object ; :: thesis: ( x in the carrier' of G implies the Source of G . x = the Source of G9 . x )
assume A38: x in the carrier' of G ; :: thesis: the Source of G . x = the Source of G9 . x
A39: now :: thesis: ( x in the carrier' of G1 implies the Source of G . x = the Source of G9 . x )
assume A40: 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 A30
.= the Source of G9 . x by A34, A40 ;
:: thesis: verum
end;
now :: thesis: ( x in the carrier' of G2 implies the Source of G . x = the Source of G9 . x )
assume A41: 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 A31
.= the Source of G9 . x by A35, A41 ;
:: thesis: verum
end;
hence the Source of G . x = the Source of G9 . x by A29, A38, A39, XBOOLE_0:def 3; :: thesis: verum
end;
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
proof
let x be object ; :: thesis: ( x in the carrier' of G implies the Target of G . x = the Target of G9 . x )
assume A43: x in the carrier' of G ; :: thesis: the Target of G . x = the Target of G9 . x
A44: now :: thesis: ( x in the carrier' of G1 implies the Target of G . x = the Target of G9 . x )
assume A45: 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 A30
.= the Target of G9 . x by A34, A45 ;
:: thesis: verum
end;
now :: thesis: ( x in the carrier' of G2 implies the Target of G . x = the Target of G9 . x )
assume A46: 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 A31
.= the Target of G9 . x by A35, A46 ;
:: thesis: verum
end;
hence the Target of G . x = the Target of G9 . x by A29, A43, A44, XBOOLE_0:def 3; :: thesis: verum
end;
hence G = G9 by A28, A29, A32, A33, A37, A42, FUNCT_1:2; :: thesis: verum