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;
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) )
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)then consider x,
y being
set such that A21:
[x,y] = v
by 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;
x in the
carrier' of
G1 \/ the
carrier' of
G2
by A22, XBOOLE_0:def 3;
then
x in the
carrier' of
(G1 \/ G2)
by A1, Def3;
then A26:
x in dom the
Source of
(G1 \/ G2)
by FUNCT_2:def 1;
the
Source of
(G1 \/ G2) . x = y
by A1, A22, A23, Def3;
hence
v in the
Source of
(G1 \/ G2)
by A21, A26, FUNCT_1:def 4;
verum end;
now assume A29:
v in the
Source of
G2
;
v in the Source of (G1 \/ G2)then consider x,
y being
set such that A30:
[x,y] = v
by 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;
x in the
carrier' of
G1 \/ the
carrier' of
G2
by A31, XBOOLE_0:def 3;
then
x in the
carrier' of
(G1 \/ G2)
by A1, Def3;
then A35:
x in dom the
Source of
(G1 \/ G2)
by FUNCT_2:def 1;
the
Source of
(G1 \/ G2) . x = y
by A1, A31, A32, Def3;
hence
v in the
Source of
(G1 \/ G2)
by A30, A35, FUNCT_1:def 4;
verum end;
hence
v in the
Source of
(G1 \/ G2)
by A18, A19, XBOOLE_0:def 3;
verum
end;
hence
the Source of (G1 \/ G2) = the Source of G1 \/ the Source of G2
by TARSKI:2; the Target of (G1 \/ G2) = the Target of G1 \/ the Target of G2
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) )
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)then consider x,
y being
set such that A56:
[x,y] = v
by 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;
x in the
carrier' of
G1 \/ the
carrier' of
G2
by A57, XBOOLE_0:def 3;
then
x in the
carrier' of
(G1 \/ G2)
by A1, Def3;
then A61:
x in dom the
Target of
(G1 \/ G2)
by FUNCT_2:def 1;
the
Target of
(G1 \/ G2) . x = y
by A1, A57, A58, Def3;
hence
v in the
Target of
(G1 \/ G2)
by A56, A61, FUNCT_1:def 4;
verum end;
now assume A64:
v in the
Target of
G2
;
v in the Target of (G1 \/ G2)then consider x,
y being
set such that A65:
[x,y] = v
by 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;
x in the
carrier' of
G1 \/ the
carrier' of
G2
by A66, XBOOLE_0:def 3;
then
x in the
carrier' of
(G1 \/ G2)
by A1, Def3;
then A70:
x in dom the
Target of
(G1 \/ G2)
by FUNCT_2:def 1;
the
Target of
(G1 \/ G2) . x = y
by A1, A66, A67, Def3;
hence
v in the
Target of
(G1 \/ G2)
by A65, A70, FUNCT_1:def 4;
verum end;
hence
v in the
Target of
(G1 \/ G2)
by A53, A54, XBOOLE_0:def 3;
verum
end;
hence
the Target of (G1 \/ G2) = the Target of G1 \/ the Target of G2
by TARSKI:2; verum