let X be non empty pathwise_connected TopSpace; :: thesis: for a1, b1, c1 being Point of X
for P1, P2 being Path of a1,b1
for Q1, Q2 being Path of b1,c1 st P1,P2 are_homotopic & Q1,Q2 are_homotopic holds
P1 + Q1,P2 + Q2 are_homotopic
let a1, b1, c1 be Point of X; :: thesis: for P1, P2 being Path of a1,b1
for Q1, Q2 being Path of b1,c1 st P1,P2 are_homotopic & Q1,Q2 are_homotopic holds
P1 + Q1,P2 + Q2 are_homotopic
let P1, P2 be Path of a1,b1; :: thesis: for Q1, Q2 being Path of b1,c1 st P1,P2 are_homotopic & Q1,Q2 are_homotopic holds
P1 + Q1,P2 + Q2 are_homotopic
let Q1, Q2 be Path of b1,c1; :: thesis: ( P1,P2 are_homotopic & Q1,Q2 are_homotopic implies P1 + Q1,P2 + Q2 are_homotopic )
( a1,b1 are_connected & b1,c1 are_connected ) by BORSUK_2:def 3;
hence ( P1,P2 are_homotopic & Q1,Q2 are_homotopic implies P1 + Q1,P2 + Q2 are_homotopic ) by Th75; :: thesis: verum