let T be non empty arcwise_connected TopSpace; :: thesis: for a, b, c being Point of T
for f being Path of a,b
for g being Path of b,c holds rng (f + g) = (rng f) \/ (rng g)
let a, b, c be Point of T; :: thesis: for f being Path of a,b
for g being Path of b,c holds rng (f + g) = (rng f) \/ (rng g)
let f be Path of a,b; :: thesis: for g being Path of b,c holds rng (f + g) = (rng f) \/ (rng g)
let g be Path of b,c; :: thesis: rng (f + g) = (rng f) \/ (rng g)
( a,b are_connected & b,c are_connected ) by BORSUK_2:def 3;
hence rng (f + g) = (rng f) \/ (rng g) by Th37; :: thesis: verum