let G1, G2, G3 be Graph; :: thesis: ( 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 A1: ( 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 ) ; :: thesis: (G1 \/ G2) \/ G3 = G1 \/ (G2 \/ G3)
A2: 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

proof

let v be set ; :: thesis: ( v in (dom the Source of (G1 \/ G2)) /\ (dom the Source of G3) implies the Source of (G1 \/ G2) . v = the Source of G3 . v )
assume A3: v in (dom the Source of (G1 \/ G2)) /\ (dom the Source of G3) ; :: thesis: the Source of (G1 \/ G2) . v = the Source of G3 . v
then A4: ( v in dom the Source of (G1 \/ G2) & v in dom the Source of G3 ) by XBOOLE_0:def 4;
v in dom the Source of (G1 \/ G2) by A3, XBOOLE_0:def 4;
then v in the carrier' of (G1 \/ G2) ;
then A5: v in the carrier' of G1 \/ the carrier' of G2 by A1, Def2;

A6: now

assume A7: v in the carrier' of G1 ; :: thesis: the Source of (G1 \/ G2) . v = the Source of G3 . v
then v in dom the Source of G1 by FUNCT_2:def 1;
then A8: v in (dom the Source of G1) /\ (dom the Source of G3) by A4, XBOOLE_0:def 4;
thus the Source of (G1 \/ G2) . v = the Source of G1 . v by A1, A7, Def2
.= the Source of G3 . v by A1, A8, PARTFUN1:def 6 ; :: thesis: verum

end;

now

assume A9: v in the carrier' of G2 ; :: thesis: the Source of (G1 \/ G2) . v = the Source of G3 . v
then v in dom the Source of G2 by FUNCT_2:def 1;
then A10: v in (dom the Source of G2) /\ (dom the Source of G3) by A4, XBOOLE_0:def 4;
thus the Source of (G1 \/ G2) . v = the Source of G2 . v by A1, A9, Def2
.= the Source of G3 . v by A1, A10, PARTFUN1:def 6 ; :: thesis: verum

end;

hence the Source of (G1 \/ G2) . v = the Source of G3 . v by A5, A6, XBOOLE_0:def 3; :: thesis: verum

end;

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

proof

let v be set ; :: thesis: ( v in (dom the Target of (G1 \/ G2)) /\ (dom the Target of G3) implies the Target of (G1 \/ G2) . v = the Target of G3 . v )
assume A11: v in (dom the Target of (G1 \/ G2)) /\ (dom the Target of G3) ; :: thesis: the Target of (G1 \/ G2) . v = the Target of G3 . v
then A12: ( v in dom the Target of (G1 \/ G2) & v in dom the Target of G3 ) by XBOOLE_0:def 4;
v in dom the Target of (G1 \/ G2) by A11, XBOOLE_0:def 4;
then v in the carrier' of (G1 \/ G2) ;
then A13: v in the carrier' of G1 \/ the carrier' of G2 by A1, Def2;

A14: now

assume A15: v in the carrier' of G1 ; :: thesis: the Target of (G1 \/ G2) . v = the Target of G3 . v
then v in dom the Target of G1 by FUNCT_2:def 1;
then A16: v in (dom the Target of G1) /\ (dom the Target of G3) by A12, XBOOLE_0:def 4;
thus the Target of (G1 \/ G2) . v = the Target of G1 . v by A1, A15, Def2
.= the Target of G3 . v by A1, A16, PARTFUN1:def 6 ; :: thesis: verum

end;

now

assume A17: v in the carrier' of G2 ; :: thesis: the Target of (G1 \/ G2) . v = the Target of G3 . v
then v in dom the Target of G2 by FUNCT_2:def 1;
then A18: v in (dom the Target of G2) /\ (dom the Target of G3) by A12, XBOOLE_0:def 4;
thus the Target of (G1 \/ G2) . v = the Target of G2 . v by A1, A17, Def2
.= the Target of G3 . v by A1, A18, PARTFUN1:def 6 ; :: thesis: verum

end;

hence the Target of (G1 \/ G2) . v = the Target of G3 . v by A13, A14, XBOOLE_0:def 3; :: thesis: verum

end;

then A19: ( the Source of (G1 \/ G2) tolerates the Source of G3 & the Target of (G1 \/ G2) tolerates the Target of G3 ) by A2, PARTFUN1:def 6;
A20: 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

proof

let v be set ; :: thesis: ( v in (dom the Source of G1) /\ (dom the Source of (G2 \/ G3)) implies the Source of G1 . v = the Source of (G2 \/ G3) . v )
assume A21: v in (dom the Source of G1) /\ (dom the Source of (G2 \/ G3)) ; :: thesis: the Source of G1 . v = the Source of (G2 \/ G3) . v
then A22: ( v in dom the Source of G1 & v in dom the Source of (G2 \/ G3) ) by XBOOLE_0:def 4;
v in the carrier' of (G2 \/ G3) by A21;
then v in the carrier' of G2 \/ the carrier' of G3 by A1, Def2;
then v in the carrier' of G2 \/ (dom the Source of G3) by FUNCT_2:def 1;
then A23: v in (dom the Source of G2) \/ (dom the Source of G3) by FUNCT_2:def 1;

A24: now

assume A25: v in dom the Source of G2 ; :: thesis: the Source of (G2 \/ G3) . v = the Source of G1 . v
A27: v in (dom the Source of G1) /\ (dom the Source of G2) by A22, A25, XBOOLE_0:def 4;
thus the Source of (G2 \/ G3) . v = the Source of G2 . v by A1, A25, Def2
.= the Source of G1 . v by A1, A27, PARTFUN1:def 6 ; :: thesis: verum

end;

now

assume A28: v in dom the Source of G3 ; :: thesis: the Source of (G2 \/ G3) . v = the Source of G1 . v
A30: v in (dom the Source of G1) /\ (dom the Source of G3) by A22, A28, XBOOLE_0:def 4;
thus the Source of (G2 \/ G3) . v = the Source of G3 . v by A1, A28, Def2
.= the Source of G1 . v by A1, A30, PARTFUN1:def 6 ; :: thesis: verum

end;

hence the Source of G1 . v = the Source of (G2 \/ G3) . v by A23, A24, XBOOLE_0:def 3; :: thesis: verum

end;

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

proof

let v be set ; :: thesis: ( v in (dom the Target of G1) /\ (dom the Target of (G2 \/ G3)) implies the Target of G1 . v = the Target of (G2 \/ G3) . v )
assume A31: v in (dom the Target of G1) /\ (dom the Target of (G2 \/ G3)) ; :: thesis: the Target of G1 . v = the Target of (G2 \/ G3) . v
then A32: ( v in dom the Target of G1 & v in dom the Target of (G2 \/ G3) ) by XBOOLE_0:def 4;
v in the carrier' of (G2 \/ G3) by A31;
then v in the carrier' of G2 \/ the carrier' of G3 by A1, Def2;
then v in the carrier' of G2 \/ (dom the Target of G3) by FUNCT_2:def 1;
then A33: v in (dom the Target of G2) \/ (dom the Target of G3) by FUNCT_2:def 1;

A34: now

assume A35: v in dom the Target of G2 ; :: thesis: the Target of (G2 \/ G3) . v = the Target of G1 . v
A37: v in (dom the Target of G1) /\ (dom the Target of G2) by A32, A35, XBOOLE_0:def 4;
thus the Target of (G2 \/ G3) . v = the Target of G2 . v by A1, A35, Def2
.= the Target of G1 . v by A1, A37, PARTFUN1:def 6 ; :: thesis: verum

end;

now

assume A38: v in dom the Target of G3 ; :: thesis: the Target of (G2 \/ G3) . v = the Target of G1 . v
A40: v in (dom the Target of G1) /\ (dom the Target of G3) by A32, A38, XBOOLE_0:def 4;
thus the Target of (G2 \/ G3) . v = the Target of G3 . v by A1, A38, Def2
.= the Target of G1 . v by A1, A40, PARTFUN1:def 6 ; :: thesis: verum

end;

hence the Target of G1 . v = the Target of (G2 \/ G3) . v by A33, A34, XBOOLE_0:def 3; :: thesis: verum

end;

then A41: ( the Source of G1 tolerates the Source of (G2 \/ G3) & the Target of G1 tolerates the Target of (G2 \/ G3) ) by A20, PARTFUN1:def 6;
A42: the carrier' of ((G1 \/ G2) \/ G3) = the carrier' of (G1 \/ G2) \/ the carrier' of G3 by A19, Def2
.= (the carrier' of G1 \/ the carrier' of G2) \/ the carrier' of G3 by A1, Def2
.= 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 A1, Def2
.= the carrier' of (G1 \/ (G2 \/ G3)) by A41, Def2 ;
A43: the carrier of ((G1 \/ G2) \/ G3) = the carrier of (G1 \/ G2) \/ the carrier of G3 by A19, Def2
.= (the carrier of G1 \/ the carrier of G2) \/ the carrier of G3 by A1, Def2
.= 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 A1, Def2
.= the carrier of (G1 \/ (G2 \/ G3)) by A41, Def2 ;
A44: dom the Source of ((G1 \/ G2) \/ G3) = the carrier' of (G1 \/ (G2 \/ G3)) by A42, 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 ; :: thesis: ( 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 A45: v in dom the Source of ((G1 \/ G2) \/ G3) ; :: thesis: 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 A19, Def2
.= (the carrier' of G1 \/ the carrier' of G2) \/ the carrier' of G3 by A1, Def2 ;
then A46: ( v in the carrier' of G1 \/ the carrier' of G2 or v in the carrier' of G3 ) by A45, XBOOLE_0:def 3;

A47: now

assume A48: v in the carrier' of G1 ; :: thesis: 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, Def2;
hence the Source of ((G1 \/ G2) \/ G3) . v = the Source of (G1 \/ G2) . v by A19, A48, Def2
.= the Source of G1 . v by A1, A48, Def2
.= the Source of (G1 \/ (G2 \/ G3)) . v by A41, A48, Def2 ;
:: thesis: verum

end;

A49: now

assume A50: v in the carrier' of G2 ; :: thesis: 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 A51: the carrier' of G2 c= the carrier' of (G1 \/ G2) by A1, Def2;
the carrier' of G2 c= the carrier' of G2 \/ the carrier' of G3 by XBOOLE_1:7;
then A52: the carrier' of G2 c= the carrier' of (G2 \/ G3) by A1, Def2;
thus the Source of ((G1 \/ G2) \/ G3) . v = the Source of (G1 \/ G2) . v by A19, A50, A51, Def2
.= the Source of G2 . v by A1, A50, Def2
.= the Source of (G2 \/ G3) . v by A1, A50, Def2
.= the Source of (G1 \/ (G2 \/ G3)) . v by A41, A50, A52, Def2 ; :: thesis: verum

end;

now

assume A53: v in the carrier' of G3 ; :: thesis: 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 A54: the carrier' of G3 c= the carrier' of (G2 \/ G3) by A1, Def2;
thus the Source of ((G1 \/ G2) \/ G3) . v = the Source of G3 . v by A19, A53, Def2
.= the Source of (G2 \/ G3) . v by A1, A53, Def2
.= the Source of (G1 \/ (G2 \/ G3)) . v by A41, A53, A54, Def2 ; :: thesis: verum

end;

hence the Source of ((G1 \/ G2) \/ G3) . v = the Source of (G1 \/ (G2 \/ G3)) . v by A46, A47, A49, XBOOLE_0:def 3; :: thesis: verum

end;

then A55: the Source of ((G1 \/ G2) \/ G3) = the Source of (G1 \/ (G2 \/ G3)) by A44, FUNCT_1:9;
A56: dom the Target of ((G1 \/ G2) \/ G3) = the carrier' of (G1 \/ (G2 \/ G3)) by A42, 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 ; :: thesis: ( 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 A57: v in dom the Target of ((G1 \/ G2) \/ G3) ; :: thesis: 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 A19, Def2
.= (the carrier' of G1 \/ the carrier' of G2) \/ the carrier' of G3 by A1, Def2 ;
then A58: ( v in the carrier' of G1 \/ the carrier' of G2 or v in the carrier' of G3 ) by A57, XBOOLE_0:def 3;

A59: now

assume A60: v in the carrier' of G1 ; :: thesis: 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, Def2;
hence the Target of ((G1 \/ G2) \/ G3) . v = the Target of (G1 \/ G2) . v by A19, A60, Def2
.= the Target of G1 . v by A1, A60, Def2
.= the Target of (G1 \/ (G2 \/ G3)) . v by A41, A60, Def2 ;
:: thesis: verum

end;

A61: now

assume A62: v in the carrier' of G2 ; :: thesis: 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 A63: the carrier' of G2 c= the carrier' of (G1 \/ G2) by A1, Def2;
the carrier' of G2 c= the carrier' of G2 \/ the carrier' of G3 by XBOOLE_1:7;
then A64: the carrier' of G2 c= the carrier' of (G2 \/ G3) by A1, Def2;
thus the Target of ((G1 \/ G2) \/ G3) . v = the Target of (G1 \/ G2) . v by A19, A62, A63, Def2
.= the Target of G2 . v by A1, A62, Def2
.= the Target of (G2 \/ G3) . v by A1, A62, Def2
.= the Target of (G1 \/ (G2 \/ G3)) . v by A41, A62, A64, Def2 ; :: thesis: verum

end;

now

assume A65: v in the carrier' of G3 ; :: thesis: 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 A66: the carrier' of G3 c= the carrier' of (G2 \/ G3) by A1, Def2;
thus the Target of ((G1 \/ G2) \/ G3) . v = the Target of G3 . v by A19, A65, Def2
.= the Target of (G2 \/ G3) . v by A1, A65, Def2
.= the Target of (G1 \/ (G2 \/ G3)) . v by A41, A65, A66, Def2 ; :: thesis: verum

end;

hence the Target of ((G1 \/ G2) \/ G3) . v = the Target of (G1 \/ (G2 \/ G3)) . v by A58, A59, A61, XBOOLE_0:def 3; :: thesis: verum

end;

hence (G1 \/ G2) \/ G3 = G1 \/ (G2 \/ G3) by A42, A43, A55, A56, FUNCT_1:9; :: thesis: verum