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 and
A2: b,c are_connected and
A3: c,d are_connected ; :: thesis: (P + Q) + R,P + (Q + R) are_homotopic
A4: a,c are_connected by A1, A2, Th46;
RePar ((P + Q) + R),3RP = P + (Q + R) by A1, A2, A3, Th60;
hence (P + Q) + R,P + (Q + R) are_homotopic by A3, A4, Th46, Th53, Th57; :: thesis: verum