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 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 ; :: thesis: (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

proof

let v be object ; :: 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 A8: 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 A9: v in dom the Source of G3 by XBOOLE_0:def 4;
v in dom the Source of (G1 \/ G2) by A8, XBOOLE_0:def 4;
then v in the carrier' of (G1 \/ G2) ;
then A10: v in the carrier' of G1 \/ the carrier' of G2 by A1, A2, Def5;

A11: now :: thesis: ( v in the carrier' of G1 implies the Source of (G1 \/ G2) . v = the Source of G3 . v )

assume A12: 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 A13: v in (dom the Source of G1) /\ (dom the Source of G3) by A9, XBOOLE_0:def 4;
thus the Source of (G1 \/ G2) . v = the Source of G1 . v by A1, A2, A12, Def5
.= the Source of G3 . v by A3, A13, PARTFUN1:def 4 ; :: thesis: verum

end;

now :: thesis: ( v in the carrier' of G2 implies the Source of (G1 \/ G2) . v = the Source of G3 . v )

assume A14: 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 A15: v in (dom the Source of G2) /\ (dom the Source of G3) by A9, XBOOLE_0:def 4;
thus the Source of (G1 \/ G2) . v = the Source of G2 . v by A1, A2, A14, Def5
.= the Source of G3 . v by A5, A15, PARTFUN1:def 4 ; :: thesis: verum

end;

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

end;

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

proof

let v be object ; :: 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 A17: 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 A18: v in dom the Target of G3 by XBOOLE_0:def 4;
v in dom the Target of (G1 \/ G2) by A17, XBOOLE_0:def 4;
then v in the carrier' of (G1 \/ G2) ;
then A19: v in the carrier' of G1 \/ the carrier' of G2 by A1, A2, Def5;

A20: now :: thesis: ( v in the carrier' of G1 implies the Target of (G1 \/ G2) . v = the Target of G3 . v )

assume A21: 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 A22: v in (dom the Target of G1) /\ (dom the Target of G3) by A18, XBOOLE_0:def 4;
thus the Target of (G1 \/ G2) . v = the Target of G1 . v by A1, A2, A21, Def5
.= the Target of G3 . v by A4, A22, PARTFUN1:def 4 ; :: thesis: verum

end;

now :: thesis: ( v in the carrier' of G2 implies the Target of (G1 \/ G2) . v = the Target of G3 . v )

assume A23: 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 A24: v in (dom the Target of G2) /\ (dom the Target of G3) by A18, XBOOLE_0:def 4;
thus the Target of (G1 \/ G2) . v = the Target of G2 . v by A1, A2, A23, Def5
.= the Target of G3 . v by A6, A24, PARTFUN1:def 4 ; :: thesis: verum

end;

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

end;

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

proof

let v be object ; :: 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 A28: 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 A29: v in dom the Source of G1 by XBOOLE_0:def 4;
v in the carrier' of (G2 \/ G3) by A28;
then v in the carrier' of G2 \/ the carrier' of G3 by A5, A6, Def5;
then v in the carrier' of G2 \/ (dom the Source of G3) by FUNCT_2:def 1;
then A30: v in (dom the Source of G2) \/ (dom the Source of G3) by FUNCT_2:def 1;

A31: now :: thesis: ( v in dom the Source of G2 implies the Source of (G2 \/ G3) . v = the Source of G1 . v )

assume A32: v in dom the Source of G2 ; :: thesis: the Source of (G2 \/ G3) . v = the Source of G1 . v
then A33: v in (dom the Source of G1) /\ (dom the Source of G2) by A29, XBOOLE_0:def 4;
thus the Source of (G2 \/ G3) . v = the Source of G2 . v by A5, A6, A32, Def5
.= the Source of G1 . v by A1, A33, PARTFUN1:def 4 ; :: thesis: verum

end;

now :: thesis: ( v in dom the Source of G3 implies the Source of (G2 \/ G3) . v = the Source of G1 . v )

assume A34: v in dom the Source of G3 ; :: thesis: the Source of (G2 \/ G3) . v = the Source of G1 . v
then A35: v in (dom the Source of G1) /\ (dom the Source of G3) by A29, XBOOLE_0:def 4;
thus the Source of (G2 \/ G3) . v = the Source of G3 . v by A5, A6, A34, Def5
.= the Source of G1 . v by A3, A35, PARTFUN1:def 4 ; :: thesis: verum

end;

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

end;

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

proof

let v be object ; :: 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 A37: 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 A38: v in dom the Target of G1 by XBOOLE_0:def 4;
v in the carrier' of (G2 \/ G3) by A37;
then v in the carrier' of G2 \/ the carrier' of G3 by A5, A6, Def5;
then v in the carrier' of G2 \/ (dom the Target of G3) by FUNCT_2:def 1;
then A39: v in (dom the Target of G2) \/ (dom the Target of G3) by FUNCT_2:def 1;

A40: now :: thesis: ( v in dom the Target of G2 implies the Target of (G2 \/ G3) . v = the Target of G1 . v )

assume A41: v in dom the Target of G2 ; :: thesis: the Target of (G2 \/ G3) . v = the Target of G1 . v
then A42: v in (dom the Target of G1) /\ (dom the Target of G2) by A38, XBOOLE_0:def 4;
thus the Target of (G2 \/ G3) . v = the Target of G2 . v by A5, A6, A41, Def5
.= the Target of G1 . v by A2, A42, PARTFUN1:def 4 ; :: thesis: verum

end;

now :: thesis: ( v in dom the Target of G3 implies the Target of (G2 \/ G3) . v = the Target of G1 . v )

assume A43: v in dom the Target of G3 ; :: thesis: the Target of (G2 \/ G3) . v = the Target of G1 . v
then A44: v in (dom the Target of G1) /\ (dom the Target of G3) by A38, XBOOLE_0:def 4;
thus the Target of (G2 \/ G3) . v = the Target of G3 . v by A5, A6, A43, Def5
.= the Target of G1 . v by A4, A44, PARTFUN1:def 4 ; :: thesis: verum

end;

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

end;

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 ; :: 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 A50: 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 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 :: thesis: ( 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 ; :: 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, 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 ;
:: thesis: verum

end;

A54: now :: thesis: ( 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 ; :: 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 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 ; :: thesis: verum

end;

now :: thesis: ( 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 ; :: 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 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 ; :: thesis: 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; :: thesis: 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 ; :: 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 A62: 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 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 :: thesis: ( 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 ; :: 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, 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 ;
:: thesis: verum

end;

A66: now :: thesis: ( 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 ; :: 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 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 ; :: thesis: verum

end;

now :: thesis: ( 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 ; :: 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 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 ; :: thesis: 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; :: thesis: verum

end;

hence (G1 \/ G2) \/ G3 = G1 \/ (G2 \/ G3) by A47, A48, A60, A61, FUNCT_1:2; :: thesis: verum