let G1, G2, G3 be Graph; ( the Source of G1 tolerates the Source of G2 & the Target of G1 tolerates the Target of G2 & the Source of G1 tolerates the Source of G3 & the Target of G1 tolerates the Target of G3 & the Source of G2 tolerates the Source of G3 & the Target of G2 tolerates the Target of G3 implies (G1 \/ G2) \/ G3 = G1 \/ (G2 \/ G3) )
assume that
A1:
the Source of G1 tolerates the Source of G2
and
A2:
the Target of G1 tolerates the Target of G2
and
A3:
the Source of G1 tolerates the Source of G3
and
A4:
the Target of G1 tolerates the Target of G3
and
A5:
the Source of G2 tolerates the Source of G3
and
A6:
the Target of G2 tolerates the Target of G3
; (G1 \/ G2) \/ G3 = G1 \/ (G2 \/ G3)
A7:
for v being set st v in (dom the Source of (G1 \/ G2)) /\ (dom the Source of G3) holds
the Source of (G1 \/ G2) . v = the Source of G3 . v
A21:
for v being set st v in (dom the Target of (G1 \/ G2)) /\ (dom the Target of G3) holds
the Target of (G1 \/ G2) . v = the Target of G3 . v
A35:
the Source of (G1 \/ G2) tolerates the Source of G3
by A7, PARTFUN1:def 6;
A36:
the Target of (G1 \/ G2) tolerates the Target of G3
by A21, PARTFUN1:def 6;
A37:
for v being set st v in (dom the Source of G1) /\ (dom the Source of (G2 \/ G3)) holds
the Source of G1 . v = the Source of (G2 \/ G3) . v
A50:
for v being set st v in (dom the Target of G1) /\ (dom the Target of (G2 \/ G3)) holds
the Target of G1 . v = the Target of (G2 \/ G3) . v
A63:
the Source of G1 tolerates the Source of (G2 \/ G3)
by A37, PARTFUN1:def 6;
A64:
the Target of G1 tolerates the Target of (G2 \/ G3)
by A50, PARTFUN1:def 6;
A65: the carrier' of ((G1 \/ G2) \/ G3) =
the carrier' of (G1 \/ G2) \/ the carrier' of G3
by A35, A36, Def3
.=
(the carrier' of G1 \/ the carrier' of G2) \/ the carrier' of G3
by A1, A2, Def3
.=
the carrier' of G1 \/ (the carrier' of G2 \/ the carrier' of G3)
by XBOOLE_1:4
.=
the carrier' of G1 \/ the carrier' of (G2 \/ G3)
by A5, A6, Def3
.=
the carrier' of (G1 \/ (G2 \/ G3))
by A63, A64, Def3
;
A66: the carrier of ((G1 \/ G2) \/ G3) =
the carrier of (G1 \/ G2) \/ the carrier of G3
by A35, A36, Def3
.=
(the carrier of G1 \/ the carrier of G2) \/ the carrier of G3
by A1, A2, Def3
.=
the carrier of G1 \/ (the carrier of G2 \/ the carrier of G3)
by XBOOLE_1:4
.=
the carrier of G1 \/ the carrier of (G2 \/ G3)
by A5, A6, Def3
.=
the carrier of (G1 \/ (G2 \/ G3))
by A63, A64, Def3
;
A67: dom the Source of ((G1 \/ G2) \/ G3) =
the carrier' of (G1 \/ (G2 \/ G3))
by A65, FUNCT_2:def 1
.=
dom the Source of (G1 \/ (G2 \/ G3))
by FUNCT_2:def 1
;
for v being set st v in dom the Source of ((G1 \/ G2) \/ G3) holds
the Source of ((G1 \/ G2) \/ G3) . v = the Source of (G1 \/ (G2 \/ G3)) . v
proof
let v be
set ;
( v in dom the Source of ((G1 \/ G2) \/ G3) implies the Source of ((G1 \/ G2) \/ G3) . v = the Source of (G1 \/ (G2 \/ G3)) . v )
assume A69:
v in dom the
Source of
((G1 \/ G2) \/ G3)
;
the Source of ((G1 \/ G2) \/ G3) . v = the Source of (G1 \/ (G2 \/ G3)) . v
dom the
Source of
((G1 \/ G2) \/ G3) =
the
carrier' of
((G1 \/ G2) \/ G3)
by FUNCT_2:def 1
.=
the
carrier' of
(G1 \/ G2) \/ the
carrier' of
G3
by A35, A36, Def3
.=
(the carrier' of G1 \/ the carrier' of G2) \/ the
carrier' of
G3
by A1, A2, Def3
;
then A71:
(
v in the
carrier' of
G1 \/ the
carrier' of
G2 or
v in the
carrier' of
G3 )
by A69, XBOOLE_0:def 3;
A72:
now assume A73:
v in the
carrier' of
G1
;
the Source of ((G1 \/ G2) \/ G3) . v = the Source of (G1 \/ (G2 \/ G3)) . v
the
carrier' of
G1 c= the
carrier' of
G1 \/ the
carrier' of
G2
by XBOOLE_1:7;
then
the
carrier' of
G1 c= the
carrier' of
(G1 \/ G2)
by A1, A2, Def3;
hence the
Source of
((G1 \/ G2) \/ G3) . v =
the
Source of
(G1 \/ G2) . v
by A35, A36, A73, Def3
.=
the
Source of
G1 . v
by A1, A2, A73, Def3
.=
the
Source of
(G1 \/ (G2 \/ G3)) . v
by A63, A64, A73, Def3
;
verum end;
A76:
now assume A77:
v in the
carrier' of
G2
;
the Source of ((G1 \/ G2) \/ G3) . v = the Source of (G1 \/ (G2 \/ G3)) . v
the
carrier' of
G2 c= the
carrier' of
G1 \/ the
carrier' of
G2
by XBOOLE_1:7;
then A79:
the
carrier' of
G2 c= the
carrier' of
(G1 \/ G2)
by A1, A2, Def3;
the
carrier' of
G2 c= the
carrier' of
G2 \/ the
carrier' of
G3
by XBOOLE_1:7;
then A81:
the
carrier' of
G2 c= the
carrier' of
(G2 \/ G3)
by A5, A6, Def3;
thus the
Source of
((G1 \/ G2) \/ G3) . v =
the
Source of
(G1 \/ G2) . v
by A35, A36, A77, A79, Def3
.=
the
Source of
G2 . v
by A1, A2, A77, Def3
.=
the
Source of
(G2 \/ G3) . v
by A5, A6, A77, Def3
.=
the
Source of
(G1 \/ (G2 \/ G3)) . v
by A63, A64, A77, A81, Def3
;
verum end;
now assume A83:
v in the
carrier' of
G3
;
the Source of ((G1 \/ G2) \/ G3) . v = the Source of (G1 \/ (G2 \/ G3)) . v
the
carrier' of
G3 c= the
carrier' of
G2 \/ the
carrier' of
G3
by XBOOLE_1:7;
then A85:
the
carrier' of
G3 c= the
carrier' of
(G2 \/ G3)
by A5, A6, Def3;
thus the
Source of
((G1 \/ G2) \/ G3) . v =
the
Source of
G3 . v
by A35, A36, A83, Def3
.=
the
Source of
(G2 \/ G3) . v
by A5, A6, A83, Def3
.=
the
Source of
(G1 \/ (G2 \/ G3)) . v
by A63, A64, A83, A85, Def3
;
verum end;
hence
the
Source of
((G1 \/ G2) \/ G3) . v = the
Source of
(G1 \/ (G2 \/ G3)) . v
by A71, A72, A76, XBOOLE_0:def 3;
verum
end;
then A86:
the Source of ((G1 \/ G2) \/ G3) = the Source of (G1 \/ (G2 \/ G3))
by A67, FUNCT_1:9;
A87: dom the Target of ((G1 \/ G2) \/ G3) =
the carrier' of (G1 \/ (G2 \/ G3))
by A65, FUNCT_2:def 1
.=
dom the Target of (G1 \/ (G2 \/ G3))
by FUNCT_2:def 1
;
for v being set st v in dom the Target of ((G1 \/ G2) \/ G3) holds
the Target of ((G1 \/ G2) \/ G3) . v = the Target of (G1 \/ (G2 \/ G3)) . v
proof
let v be
set ;
( v in dom the Target of ((G1 \/ G2) \/ G3) implies the Target of ((G1 \/ G2) \/ G3) . v = the Target of (G1 \/ (G2 \/ G3)) . v )
assume A89:
v in dom the
Target of
((G1 \/ G2) \/ G3)
;
the Target of ((G1 \/ G2) \/ G3) . v = the Target of (G1 \/ (G2 \/ G3)) . v
dom the
Target of
((G1 \/ G2) \/ G3) =
the
carrier' of
((G1 \/ G2) \/ G3)
by FUNCT_2:def 1
.=
the
carrier' of
(G1 \/ G2) \/ the
carrier' of
G3
by A35, A36, Def3
.=
(the carrier' of G1 \/ the carrier' of G2) \/ the
carrier' of
G3
by A1, A2, Def3
;
then A91:
(
v in the
carrier' of
G1 \/ the
carrier' of
G2 or
v in the
carrier' of
G3 )
by A89, XBOOLE_0:def 3;
A92:
now assume A93:
v in the
carrier' of
G1
;
the Target of ((G1 \/ G2) \/ G3) . v = the Target of (G1 \/ (G2 \/ G3)) . v
the
carrier' of
G1 c= the
carrier' of
G1 \/ the
carrier' of
G2
by XBOOLE_1:7;
then
the
carrier' of
G1 c= the
carrier' of
(G1 \/ G2)
by A1, A2, Def3;
hence the
Target of
((G1 \/ G2) \/ G3) . v =
the
Target of
(G1 \/ G2) . v
by A35, A36, A93, Def3
.=
the
Target of
G1 . v
by A1, A2, A93, Def3
.=
the
Target of
(G1 \/ (G2 \/ G3)) . v
by A63, A64, A93, Def3
;
verum end;
A96:
now assume A97:
v in the
carrier' of
G2
;
the Target of ((G1 \/ G2) \/ G3) . v = the Target of (G1 \/ (G2 \/ G3)) . v
the
carrier' of
G2 c= the
carrier' of
G1 \/ the
carrier' of
G2
by XBOOLE_1:7;
then A99:
the
carrier' of
G2 c= the
carrier' of
(G1 \/ G2)
by A1, A2, Def3;
the
carrier' of
G2 c= the
carrier' of
G2 \/ the
carrier' of
G3
by XBOOLE_1:7;
then A101:
the
carrier' of
G2 c= the
carrier' of
(G2 \/ G3)
by A5, A6, Def3;
thus the
Target of
((G1 \/ G2) \/ G3) . v =
the
Target of
(G1 \/ G2) . v
by A35, A36, A97, A99, Def3
.=
the
Target of
G2 . v
by A1, A2, A97, Def3
.=
the
Target of
(G2 \/ G3) . v
by A5, A6, A97, Def3
.=
the
Target of
(G1 \/ (G2 \/ G3)) . v
by A63, A64, A97, A101, Def3
;
verum end;
now assume A103:
v in the
carrier' of
G3
;
the Target of ((G1 \/ G2) \/ G3) . v = the Target of (G1 \/ (G2 \/ G3)) . v
the
carrier' of
G3 c= the
carrier' of
G2 \/ the
carrier' of
G3
by XBOOLE_1:7;
then A105:
the
carrier' of
G3 c= the
carrier' of
(G2 \/ G3)
by A5, A6, Def3;
thus the
Target of
((G1 \/ G2) \/ G3) . v =
the
Target of
G3 . v
by A35, A36, A103, Def3
.=
the
Target of
(G2 \/ G3) . v
by A5, A6, A103, Def3
.=
the
Target of
(G1 \/ (G2 \/ G3)) . v
by A63, A64, A103, A105, Def3
;
verum end;
hence
the
Target of
((G1 \/ G2) \/ G3) . v = the
Target of
(G1 \/ (G2 \/ G3)) . v
by A91, A92, A96, XBOOLE_0:def 3;
verum
end;
hence
(G1 \/ G2) \/ G3 = G1 \/ (G2 \/ G3)
by A65, A66, A86, A87, FUNCT_1:9; verum