let T be non empty pathwise_connected TopSpace; for a, b, c, d being Point of T
for f being Path of a,b
for g being Path of b,c
for h being Path of c,d holds rng ((f + g) + h) = ((rng f) \/ (rng g)) \/ (rng h)
let a, b, c, d be Point of T; for f being Path of a,b
for g being Path of b,c
for h being Path of c,d holds rng ((f + g) + h) = ((rng f) \/ (rng g)) \/ (rng h)
let f be Path of a,b; for g being Path of b,c
for h being Path of c,d holds rng ((f + g) + h) = ((rng f) \/ (rng g)) \/ (rng h)
let g be Path of b,c; for h being Path of c,d holds rng ((f + g) + h) = ((rng f) \/ (rng g)) \/ (rng h)
let h be Path of c,d; rng ((f + g) + h) = ((rng f) \/ (rng g)) \/ (rng h)
A1:
a,b are_connected
by BORSUK_2:def 3;
A2:
b,c are_connected
by BORSUK_2:def 3;
c,d are_connected
by BORSUK_2:def 3;
hence
rng ((f + g) + h) = ((rng f) \/ (rng g)) \/ (rng h)
by A1, A2, Th39; verum