let S, T be non empty pathwise_connected TopSpace; :: thesis: 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)
let s1, s2, s3 be Point of S; :: thesis: 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)
let t1, t2, t3 be Point of T; :: thesis: 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)
let l1 be Path of [s1,t1],[s2,t2]; :: thesis: for l2 being Path of [s2,t2],[s3,t3] holds pr2 (l1 + l2) = (pr2 l1) + (pr2 l2)
let l2 be Path of [s2,t2],[s3,t3]; :: thesis: pr2 (l1 + l2) = (pr2 l1) + (pr2 l2)
( [s1,t1],[s2,t2] are_connected & [s2,t2],[s3,t3] are_connected ) by BORSUK_2:def 3;
hence pr2 (l1 + l2) = (pr2 l1) + (pr2 l2) by Th25; :: thesis: verum