let T be non empty TopSpace; :: thesis: for a, b, c, d being Point of T
for P being Path of a,b
for Q being Path of b,c
for R being Path of c,d st a,b are_connected & b,c are_connected & c,d are_connected holds
(P + Q) + R,P + (Q + R) are_homotopic
let a, b, c, d be Point of T; :: thesis: for P being Path of a,b
for Q being Path of b,c
for R being Path of c,d st a,b are_connected & b,c are_connected & c,d are_connected holds
(P + Q) + R,P + (Q + R) are_homotopic
let P be Path of a,b; :: thesis: for Q being Path of b,c
for R being Path of c,d st a,b are_connected & b,c are_connected & c,d are_connected holds
(P + Q) + R,P + (Q + R) are_homotopic
let Q be Path of b,c; :: thesis: for R being Path of c,d st a,b are_connected & b,c are_connected & c,d are_connected holds
(P + Q) + R,P + (Q + R) are_homotopic
let R be Path of c,d; :: thesis: ( a,b are_connected & b,c are_connected & c,d are_connected implies (P + Q) + R,P + (Q + R) are_homotopic )
assume that
A1: ( a,b are_connected & b,c are_connected ) and
A2: c,d are_connected ; :: thesis: (P + Q) + R,P + (Q + R) are_homotopic
( a,c are_connected & RePar (((P + Q) + R),3RP) = P + (Q + R) ) by A1, A2, Th42, Th52;
hence (P + Q) + R,P + (Q + R) are_homotopic by A2, Th42, Th45, Th49; :: thesis: verum