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 object 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
A16:
for v being object 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
A25:
the Source of (G1 \/ G2) tolerates the Source of G3
by A7, PARTFUN1:def 4;
A26:
the Target of (G1 \/ G2) tolerates the Target of G3
by A16, PARTFUN1:def 4;
A27:
for v being object 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
A36:
for v being object 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
A45:
the Source of G1 tolerates the Source of (G2 \/ G3)
by A27, PARTFUN1:def 4;
A46:
the Target of G1 tolerates the Target of (G2 \/ G3)
by A36, PARTFUN1:def 4;
A47: the carrier' of ((G1 \/ G2) \/ G3) =
the carrier' of (G1 \/ G2) \/ the carrier' of G3
by A25, A26, Def5
.=
( the carrier' of G1 \/ the carrier' of G2) \/ the carrier' of G3
by A1, A2, Def5
.=
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, Def5
.=
the carrier' of (G1 \/ (G2 \/ G3))
by A45, A46, Def5
;
A48: the carrier of ((G1 \/ G2) \/ G3) =
the carrier of (G1 \/ G2) \/ the carrier of G3
by A25, A26, Def5
.=
( the carrier of G1 \/ the carrier of G2) \/ the carrier of G3
by A1, A2, Def5
.=
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, Def5
.=
the carrier of (G1 \/ (G2 \/ G3))
by A45, A46, Def5
;
A49: dom the Source of ((G1 \/ G2) \/ G3) =
the carrier' of (G1 \/ (G2 \/ G3))
by A47, FUNCT_2:def 1
.=
dom the Source of (G1 \/ (G2 \/ G3))
by FUNCT_2:def 1
;
for v being object 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
object ;
( 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 A50:
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 A25, A26, Def5
.=
( the carrier' of G1 \/ the carrier' of G2) \/ the
carrier' of
G3
by A1, A2, Def5
;
then A51:
(
v in the
carrier' of
G1 \/ the
carrier' of
G2 or
v in the
carrier' of
G3 )
by A50, XBOOLE_0:def 3;
A52:
now ( v in the carrier' of G1 implies the Source of ((G1 \/ G2) \/ G3) . v = the Source of (G1 \/ (G2 \/ G3)) . v )assume A53:
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, Def5;
hence the
Source of
((G1 \/ G2) \/ G3) . v =
the
Source of
(G1 \/ G2) . v
by A25, A26, A53, Def5
.=
the
Source of
G1 . v
by A1, A2, A53, Def5
.=
the
Source of
(G1 \/ (G2 \/ G3)) . v
by A45, A46, A53, Def5
;
verum end;
A54:
now ( v in the carrier' of G2 implies the Source of ((G1 \/ G2) \/ G3) . v = the Source of (G1 \/ (G2 \/ G3)) . v )assume A55:
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 A56:
the
carrier' of
G2 c= the
carrier' of
(G1 \/ G2)
by A1, A2, Def5;
the
carrier' of
G2 c= the
carrier' of
G2 \/ the
carrier' of
G3
by XBOOLE_1:7;
then A57:
the
carrier' of
G2 c= the
carrier' of
(G2 \/ G3)
by A5, A6, Def5;
thus the
Source of
((G1 \/ G2) \/ G3) . v =
the
Source of
(G1 \/ G2) . v
by A25, A26, A55, A56, Def5
.=
the
Source of
G2 . v
by A1, A2, A55, Def5
.=
the
Source of
(G2 \/ G3) . v
by A5, A6, A55, Def5
.=
the
Source of
(G1 \/ (G2 \/ G3)) . v
by A45, A46, A55, A57, Def5
;
verum end;
now ( v in the carrier' of G3 implies the Source of ((G1 \/ G2) \/ G3) . v = the Source of (G1 \/ (G2 \/ G3)) . v )assume A58:
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 A59:
the
carrier' of
G3 c= the
carrier' of
(G2 \/ G3)
by A5, A6, Def5;
thus the
Source of
((G1 \/ G2) \/ G3) . v =
the
Source of
G3 . v
by A25, A26, A58, Def5
.=
the
Source of
(G2 \/ G3) . v
by A5, A6, A58, Def5
.=
the
Source of
(G1 \/ (G2 \/ G3)) . v
by A45, A46, A58, A59, Def5
;
verum end;
hence
the
Source of
((G1 \/ G2) \/ G3) . v = the
Source of
(G1 \/ (G2 \/ G3)) . v
by A51, A52, A54, XBOOLE_0:def 3;
verum
end;
then A60:
the Source of ((G1 \/ G2) \/ G3) = the Source of (G1 \/ (G2 \/ G3))
by A49;
A61: dom the Target of ((G1 \/ G2) \/ G3) =
the carrier' of (G1 \/ (G2 \/ G3))
by A47, FUNCT_2:def 1
.=
dom the Target of (G1 \/ (G2 \/ G3))
by FUNCT_2:def 1
;
for v being object 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
object ;
( 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 A62:
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 A25, A26, Def5
.=
( the carrier' of G1 \/ the carrier' of G2) \/ the
carrier' of
G3
by A1, A2, Def5
;
then A63:
(
v in the
carrier' of
G1 \/ the
carrier' of
G2 or
v in the
carrier' of
G3 )
by A62, XBOOLE_0:def 3;
A64:
now ( v in the carrier' of G1 implies the Target of ((G1 \/ G2) \/ G3) . v = the Target of (G1 \/ (G2 \/ G3)) . v )assume A65:
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, Def5;
hence the
Target of
((G1 \/ G2) \/ G3) . v =
the
Target of
(G1 \/ G2) . v
by A25, A26, A65, Def5
.=
the
Target of
G1 . v
by A1, A2, A65, Def5
.=
the
Target of
(G1 \/ (G2 \/ G3)) . v
by A45, A46, A65, Def5
;
verum end;
A66:
now ( v in the carrier' of G2 implies the Target of ((G1 \/ G2) \/ G3) . v = the Target of (G1 \/ (G2 \/ G3)) . v )assume A67:
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 A68:
the
carrier' of
G2 c= the
carrier' of
(G1 \/ G2)
by A1, A2, Def5;
the
carrier' of
G2 c= the
carrier' of
G2 \/ the
carrier' of
G3
by XBOOLE_1:7;
then A69:
the
carrier' of
G2 c= the
carrier' of
(G2 \/ G3)
by A5, A6, Def5;
thus the
Target of
((G1 \/ G2) \/ G3) . v =
the
Target of
(G1 \/ G2) . v
by A25, A26, A67, A68, Def5
.=
the
Target of
G2 . v
by A1, A2, A67, Def5
.=
the
Target of
(G2 \/ G3) . v
by A5, A6, A67, Def5
.=
the
Target of
(G1 \/ (G2 \/ G3)) . v
by A45, A46, A67, A69, Def5
;
verum end;
now ( v in the carrier' of G3 implies the Target of ((G1 \/ G2) \/ G3) . v = the Target of (G1 \/ (G2 \/ G3)) . v )assume A70:
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 A71:
the
carrier' of
G3 c= the
carrier' of
(G2 \/ G3)
by A5, A6, Def5;
thus the
Target of
((G1 \/ G2) \/ G3) . v =
the
Target of
G3 . v
by A25, A26, A70, Def5
.=
the
Target of
(G2 \/ G3) . v
by A5, A6, A70, Def5
.=
the
Target of
(G1 \/ (G2 \/ G3)) . v
by A45, A46, A70, A71, Def5
;
verum end;
hence
the
Target of
((G1 \/ G2) \/ G3) . v = the
Target of
(G1 \/ (G2 \/ G3)) . v
by A63, A64, A66, XBOOLE_0:def 3;
verum
end;
hence
(G1 \/ G2) \/ G3 = G1 \/ (G2 \/ G3)
by A47, A48, A60, A61, FUNCT_1:2; verum