theorem Th75:
for
T being non
empty TopSpace for
a,
b,
c being
Point of
T for
P1,
P2 being
Path of
a,
b for
Q1,
Q2 being
Path of
b,
c st
a,
b are_connected &
b,
c are_connected &
P1,
P2 are_homotopic &
Q1,
Q2 are_homotopic holds
P1 + Q1,
P2 + Q2 are_homotopic