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 pr2 (l1 + l2) = (pr2 l1) + (pr2 l2)