theorem :: TOPALG_4:24

for S, T being non empty pathwise_connected TopSpace
for s1, s2, s3 being Point of S
for t1, t2, t3 being Point of T
for l1 being Path of [s1,t1],[s2,t2]
for l2 being Path of [s2,t2],[s3,t3] holds pr1 (l1 + l2) = (pr1 l1) + (pr1 l2)