let G1, G2 be Graph; :: thesis: ( 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 )
; :: thesis: ( 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 ;
:: thesis: ( 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 )
:: thesis: ( v in the Source of G1 \/ the Source of G2 implies v in the Source of (G1 \/ G2) )
assume A10:
v in the
Source of
G1 \/ the
Source of
G2
;
:: thesis: v in the Source of (G1 \/ G2)
A11:
now assume A12:
v in the
Source of
G1
;
:: thesis: v in the Source of (G1 \/ G2)then consider x,
y being
set such that A13:
[x,y] = v
by RELAT_1:def 1;
A14:
(
x in dom the
Source of
G1 &
y = the
Source of
G1 . x )
by A12, A13, FUNCT_1:8;
x in the
carrier' of
G1 \/ the
carrier' of
G2
by A14, XBOOLE_0:def 3;
then
x in the
carrier' of
(G1 \/ G2)
by A1, Def2;
then A16:
x in dom the
Source of
(G1 \/ G2)
by FUNCT_2:def 1;
the
Source of
(G1 \/ G2) . x = y
by A1, A14, Def2;
hence
v in the
Source of
(G1 \/ G2)
by A13, A16, FUNCT_1:def 4;
:: thesis: verum end;
now assume A17:
v in the
Source of
G2
;
:: thesis: v in the Source of (G1 \/ G2)then consider x,
y being
set such that A18:
[x,y] = v
by RELAT_1:def 1;
A19:
(
x in dom the
Source of
G2 &
y = the
Source of
G2 . x )
by A17, A18, FUNCT_1:8;
x in the
carrier' of
G1 \/ the
carrier' of
G2
by A19, XBOOLE_0:def 3;
then
x in the
carrier' of
(G1 \/ G2)
by A1, Def2;
then A21:
x in dom the
Source of
(G1 \/ G2)
by FUNCT_2:def 1;
the
Source of
(G1 \/ G2) . x = y
by A1, A19, Def2;
hence
v in the
Source of
(G1 \/ G2)
by A18, A21, FUNCT_1:def 4;
:: thesis: verum end;
hence
v in the
Source of
(G1 \/ G2)
by A10, A11, XBOOLE_0:def 3;
:: thesis: verum
end;
hence
the Source of (G1 \/ G2) = the Source of G1 \/ the Source of G2
by TARSKI:2; :: thesis: 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 ;
:: thesis: ( 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 )
:: thesis: ( v in the Target of G1 \/ the Target of G2 implies v in the Target of (G1 \/ G2) )
assume A30:
v in the
Target of
G1 \/ the
Target of
G2
;
:: thesis: v in the Target of (G1 \/ G2)
A31:
now assume A32:
v in the
Target of
G1
;
:: thesis: v in the Target of (G1 \/ G2)then consider x,
y being
set such that A33:
[x,y] = v
by RELAT_1:def 1;
A34:
(
x in dom the
Target of
G1 &
y = the
Target of
G1 . x )
by A32, A33, FUNCT_1:8;
x in the
carrier' of
G1 \/ the
carrier' of
G2
by A34, XBOOLE_0:def 3;
then
x in the
carrier' of
(G1 \/ G2)
by A1, Def2;
then A36:
x in dom the
Target of
(G1 \/ G2)
by FUNCT_2:def 1;
the
Target of
(G1 \/ G2) . x = y
by A1, A34, Def2;
hence
v in the
Target of
(G1 \/ G2)
by A33, A36, FUNCT_1:def 4;
:: thesis: verum end;
now assume A37:
v in the
Target of
G2
;
:: thesis: v in the Target of (G1 \/ G2)then consider x,
y being
set such that A38:
[x,y] = v
by RELAT_1:def 1;
A39:
(
x in dom the
Target of
G2 &
y = the
Target of
G2 . x )
by A37, A38, FUNCT_1:8;
x in the
carrier' of
G1 \/ the
carrier' of
G2
by A39, XBOOLE_0:def 3;
then
x in the
carrier' of
(G1 \/ G2)
by A1, Def2;
then A41:
x in dom the
Target of
(G1 \/ G2)
by FUNCT_2:def 1;
the
Target of
(G1 \/ G2) . x = y
by A1, A39, Def2;
hence
v in the
Target of
(G1 \/ G2)
by A38, A41, FUNCT_1:def 4;
:: thesis: verum end;
hence
v in the
Target of
(G1 \/ G2)
by A30, A31, XBOOLE_0:def 3;
:: thesis: verum
end;
hence
the Target of (G1 \/ G2) = the Target of G1 \/ the Target of G2
by TARSKI:2; :: thesis: verum