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 object holds
( v in the Source of (G1 \/ G2) iff v in the Source of G1 \/ the Source of G2 )
proof
let v be
object ;
( 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 A10:
v in the
Source of
G1 \/ the
Source of
G2
;
v in the Source of (G1 \/ G2)
A11:
now ( v in the Source of G1 implies v in the Source of (G1 \/ G2) )assume A12:
v in the
Source of
G1
;
v in the Source of (G1 \/ G2)then consider x,
y being
object such that A13:
[x,y] = v
by RELAT_1:def 1;
A14:
x in dom the
Source of
G1
by A12, A13, FUNCT_1:1;
A15:
y = the
Source of
G1 . x
by A12, A13, FUNCT_1:1;
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, Def5;
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, A15, Def5;
hence
v in the
Source of
(G1 \/ G2)
by A13, A16, FUNCT_1:def 2;
verum end;
now ( v in the Source of G2 implies v in the Source of (G1 \/ G2) )assume A17:
v in the
Source of
G2
;
v in the Source of (G1 \/ G2)then consider x,
y being
object such that A18:
[x,y] = v
by RELAT_1:def 1;
A19:
x in dom the
Source of
G2
by A17, A18, FUNCT_1:1;
A20:
y = the
Source of
G2 . x
by A17, A18, FUNCT_1:1;
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, Def5;
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, A20, Def5;
hence
v in the
Source of
(G1 \/ G2)
by A18, A21, FUNCT_1:def 2;
verum end;
hence
v in the
Source of
(G1 \/ G2)
by A10, A11, 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 object holds
( v in the Target of (G1 \/ G2) iff v in the Target of G1 \/ the Target of G2 )
proof
let v be
object ;
( 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 A30:
v in the
Target of
G1 \/ the
Target of
G2
;
v in the Target of (G1 \/ G2)
A31:
now ( v in the Target of G1 implies v in the Target of (G1 \/ G2) )assume A32:
v in the
Target of
G1
;
v in the Target of (G1 \/ G2)then consider x,
y being
object such that A33:
[x,y] = v
by RELAT_1:def 1;
A34:
x in dom the
Target of
G1
by A32, A33, FUNCT_1:1;
A35:
y = the
Target of
G1 . x
by A32, A33, FUNCT_1:1;
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, Def5;
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, A35, Def5;
hence
v in the
Target of
(G1 \/ G2)
by A33, A36, FUNCT_1:def 2;
verum end;
now ( v in the Target of G2 implies v in the Target of (G1 \/ G2) )assume A37:
v in the
Target of
G2
;
v in the Target of (G1 \/ G2)then consider x,
y being
object such that A38:
[x,y] = v
by RELAT_1:def 1;
A39:
x in dom the
Target of
G2
by A37, A38, FUNCT_1:1;
A40:
y = the
Target of
G2 . x
by A37, A38, FUNCT_1:1;
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, Def5;
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, A40, Def5;
hence
v in the
Target of
(G1 \/ G2)
by A38, A41, FUNCT_1:def 2;
verum end;
hence
v in the
Target of
(G1 \/ G2)
by A30, A31, XBOOLE_0:def 3;
verum
end;
hence
the Target of (G1 \/ G2) = the Target of G1 \/ the Target of G2
by TARSKI:2; verum