let G1, G2 be Graph; ( the Source of G1 tolerates the Source of G2 & the Target of G1 tolerates the Target of G2 implies ( the Source of (G1 \/ G2) = the Source of G1 \/ the Source of G2 & the Target of (G1 \/ G2) = the Target of G1 \/ the Target of G2 ) )
assume A1:
( the Source of G1 tolerates the Source of G2 & the Target of G1 tolerates the Target of G2 )
; ( the Source of (G1 \/ G2) = the Source of G1 \/ the Source of G2 & the Target of (G1 \/ G2) = the Target of G1 \/ the Target of G2 )
set S12 = the Source of (G1 \/ G2);
set S1 = the Source of G1;
set S2 = the Source of G2;
set T12 = the Target of (G1 \/ G2);
set T1 = the Target of G1;
set T2 = the Target of G2;
A2:
for v being set holds
( v in the Source of (G1 \/ G2) iff v in the Source of G1 \/ the Source of G2 )
proof
let v be
set ;
( v in the Source of (G1 \/ G2) iff v in the Source of G1 \/ the Source of G2 )
thus
(
v in the
Source of
(G1 \/ G2) implies
v in the
Source of
G1 \/ the
Source of
G2 )
( v in the Source of G1 \/ the Source of G2 implies v in the Source of (G1 \/ G2) )proof
assume A3:
v in the
Source of
(G1 \/ G2)
;
v in the Source of G1 \/ the Source of G2
consider x,
y being
set such that A4:
[x,y] = v
by A3, RELAT_1:def 1;
A5:
x in dom the
Source of
(G1 \/ G2)
by A3, A4, FUNCT_1:8;
A6:
x in the
carrier' of
(G1 \/ G2)
by A5;
A7:
x in the
carrier' of
G1 \/ the
carrier' of
G2
by A1, A6, Def3;
A8:
now assume A9:
x in the
carrier' of
G1
;
[x,y] in the Source of G1 \/ the Source of G2A10:
x in dom the
Source of
G1
by A9, FUNCT_2:def 1;
A11: the
Source of
G1 . x =
the
Source of
(G1 \/ G2) . x
by A1, A9, Def3
.=
y
by A3, A4, FUNCT_1:8
;
A12:
(
[x,y] in the
Source of
G1 or
[x,y] in the
Source of
G2 )
by A10, A11, FUNCT_1:def 4;
thus
[x,y] in the
Source of
G1 \/ the
Source of
G2
by A12, XBOOLE_0:def 3;
verum end;
A13:
now assume A14:
x in the
carrier' of
G2
;
[x,y] in the Source of G1 \/ the Source of G2A15:
x in dom the
Source of
G2
by A14, FUNCT_2:def 1;
A16: the
Source of
G2 . x =
the
Source of
(G1 \/ G2) . x
by A1, A14, Def3
.=
y
by A3, A4, FUNCT_1:8
;
A17:
(
[x,y] in the
Source of
G1 or
[x,y] in the
Source of
G2 )
by A15, A16, FUNCT_1:def 4;
thus
[x,y] in the
Source of
G1 \/ the
Source of
G2
by A17, XBOOLE_0:def 3;
verum end;
thus
v in the
Source of
G1 \/ the
Source of
G2
by A4, A7, A8, A13, XBOOLE_0:def 3;
verum
end;
assume A18:
v in the
Source of
G1 \/ the
Source of
G2
;
v in the Source of (G1 \/ G2)
A19:
now assume A20:
v in the
Source of
G1
;
v in the Source of (G1 \/ G2)consider x,
y being
set such that A21:
[x,y] = v
by A20, RELAT_1:def 1;
A22:
x in dom the
Source of
G1
by A20, A21, FUNCT_1:8;
A23:
y = the
Source of
G1 . x
by A20, A21, FUNCT_1:8;
A24:
x in the
carrier' of
G1 \/ the
carrier' of
G2
by A22, XBOOLE_0:def 3;
A25:
x in the
carrier' of
(G1 \/ G2)
by A1, A24, Def3;
A26:
x in dom the
Source of
(G1 \/ G2)
by A25, FUNCT_2:def 1;
A27:
the
Source of
(G1 \/ G2) . x = y
by A1, A22, A23, Def3;
thus
v in the
Source of
(G1 \/ G2)
by A21, A26, A27, FUNCT_1:def 4;
verum end;
A28:
now assume A29:
v in the
Source of
G2
;
v in the Source of (G1 \/ G2)consider x,
y being
set such that A30:
[x,y] = v
by A29, RELAT_1:def 1;
A31:
x in dom the
Source of
G2
by A29, A30, FUNCT_1:8;
A32:
y = the
Source of
G2 . x
by A29, A30, FUNCT_1:8;
A33:
x in the
carrier' of
G1 \/ the
carrier' of
G2
by A31, XBOOLE_0:def 3;
A34:
x in the
carrier' of
(G1 \/ G2)
by A1, A33, Def3;
A35:
x in dom the
Source of
(G1 \/ G2)
by A34, FUNCT_2:def 1;
A36:
the
Source of
(G1 \/ G2) . x = y
by A1, A31, A32, Def3;
thus
v in the
Source of
(G1 \/ G2)
by A30, A35, A36, FUNCT_1:def 4;
verum end;
thus
v in the
Source of
(G1 \/ G2)
by A18, A19, A28, XBOOLE_0:def 3;
verum
end;
thus
the Source of (G1 \/ G2) = the Source of G1 \/ the Source of G2
by A2, TARSKI:2; the Target of (G1 \/ G2) = the Target of G1 \/ the Target of G2
A37:
for v being set holds
( v in the Target of (G1 \/ G2) iff v in the Target of G1 \/ the Target of G2 )
proof
let v be
set ;
( v in the Target of (G1 \/ G2) iff v in the Target of G1 \/ the Target of G2 )
thus
(
v in the
Target of
(G1 \/ G2) implies
v in the
Target of
G1 \/ the
Target of
G2 )
( v in the Target of G1 \/ the Target of G2 implies v in the Target of (G1 \/ G2) )proof
assume A38:
v in the
Target of
(G1 \/ G2)
;
v in the Target of G1 \/ the Target of G2
consider x,
y being
set such that A39:
[x,y] = v
by A38, RELAT_1:def 1;
A40:
x in dom the
Target of
(G1 \/ G2)
by A38, A39, FUNCT_1:8;
A41:
x in the
carrier' of
(G1 \/ G2)
by A40;
A42:
x in the
carrier' of
G1 \/ the
carrier' of
G2
by A1, A41, Def3;
A43:
now assume A44:
x in the
carrier' of
G1
;
[x,y] in the Target of G1 \/ the Target of G2A45:
x in dom the
Target of
G1
by A44, FUNCT_2:def 1;
A46: the
Target of
G1 . x =
the
Target of
(G1 \/ G2) . x
by A1, A44, Def3
.=
y
by A38, A39, FUNCT_1:8
;
A47:
(
[x,y] in the
Target of
G1 or
[x,y] in the
Target of
G2 )
by A45, A46, FUNCT_1:def 4;
thus
[x,y] in the
Target of
G1 \/ the
Target of
G2
by A47, XBOOLE_0:def 3;
verum end;
A48:
now assume A49:
x in the
carrier' of
G2
;
[x,y] in the Target of G1 \/ the Target of G2A50:
x in dom the
Target of
G2
by A49, FUNCT_2:def 1;
A51: the
Target of
G2 . x =
the
Target of
(G1 \/ G2) . x
by A1, A49, Def3
.=
y
by A38, A39, FUNCT_1:8
;
A52:
(
[x,y] in the
Target of
G1 or
[x,y] in the
Target of
G2 )
by A50, A51, FUNCT_1:def 4;
thus
[x,y] in the
Target of
G1 \/ the
Target of
G2
by A52, XBOOLE_0:def 3;
verum end;
thus
v in the
Target of
G1 \/ the
Target of
G2
by A39, A42, A43, A48, XBOOLE_0:def 3;
verum
end;
assume A53:
v in the
Target of
G1 \/ the
Target of
G2
;
v in the Target of (G1 \/ G2)
A54:
now assume A55:
v in the
Target of
G1
;
v in the Target of (G1 \/ G2)consider x,
y being
set such that A56:
[x,y] = v
by A55, RELAT_1:def 1;
A57:
x in dom the
Target of
G1
by A55, A56, FUNCT_1:8;
A58:
y = the
Target of
G1 . x
by A55, A56, FUNCT_1:8;
A59:
x in the
carrier' of
G1 \/ the
carrier' of
G2
by A57, XBOOLE_0:def 3;
A60:
x in the
carrier' of
(G1 \/ G2)
by A1, A59, Def3;
A61:
x in dom the
Target of
(G1 \/ G2)
by A60, FUNCT_2:def 1;
A62:
the
Target of
(G1 \/ G2) . x = y
by A1, A57, A58, Def3;
thus
v in the
Target of
(G1 \/ G2)
by A56, A61, A62, FUNCT_1:def 4;
verum end;
A63:
now assume A64:
v in the
Target of
G2
;
v in the Target of (G1 \/ G2)consider x,
y being
set such that A65:
[x,y] = v
by A64, RELAT_1:def 1;
A66:
x in dom the
Target of
G2
by A64, A65, FUNCT_1:8;
A67:
y = the
Target of
G2 . x
by A64, A65, FUNCT_1:8;
A68:
x in the
carrier' of
G1 \/ the
carrier' of
G2
by A66, XBOOLE_0:def 3;
A69:
x in the
carrier' of
(G1 \/ G2)
by A1, A68, Def3;
A70:
x in dom the
Target of
(G1 \/ G2)
by A69, FUNCT_2:def 1;
A71:
the
Target of
(G1 \/ G2) . x = y
by A1, A66, A67, Def3;
thus
v in the
Target of
(G1 \/ G2)
by A65, A70, A71, FUNCT_1:def 4;
verum end;
thus
v in the
Target of
(G1 \/ G2)
by A53, A54, A63, XBOOLE_0:def 3;
verum
end;
thus
the Target of (G1 \/ G2) = the Target of G1 \/ the Target of G2
by A37, TARSKI:2; verum