let T be non empty pathwise_connected TopSpace; :: thesis: for a, b, c, d, e, z 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
for i being Path of d,e
for j being Path of e,z holds rng ((((f + g) + h) + i) + j) = ((((rng f) \/ (rng g)) \/ (rng h)) \/ (rng i)) \/ (rng j)
let a, b, c, d, e, z be Point of T; :: thesis: for f being Path of a,b
for g being Path of b,c
for h being Path of c,d
for i being Path of d,e
for j being Path of e,z holds rng ((((f + g) + h) + i) + j) = ((((rng f) \/ (rng g)) \/ (rng h)) \/ (rng i)) \/ (rng j)
let f be Path of a,b; :: thesis: for g being Path of b,c
for h being Path of c,d
for i being Path of d,e
for j being Path of e,z holds rng ((((f + g) + h) + i) + j) = ((((rng f) \/ (rng g)) \/ (rng h)) \/ (rng i)) \/ (rng j)
let g be Path of b,c; :: thesis: for h being Path of c,d
for i being Path of d,e
for j being Path of e,z holds rng ((((f + g) + h) + i) + j) = ((((rng f) \/ (rng g)) \/ (rng h)) \/ (rng i)) \/ (rng j)
let h be Path of c,d; :: thesis: for i being Path of d,e
for j being Path of e,z holds rng ((((f + g) + h) + i) + j) = ((((rng f) \/ (rng g)) \/ (rng h)) \/ (rng i)) \/ (rng j)
let i be Path of d,e; :: thesis: for j being Path of e,z holds rng ((((f + g) + h) + i) + j) = ((((rng f) \/ (rng g)) \/ (rng h)) \/ (rng i)) \/ (rng j)
let j be Path of e,z; :: thesis: rng ((((f + g) + h) + i) + j) = ((((rng f) \/ (rng g)) \/ (rng h)) \/ (rng i)) \/ (rng j)
A1: a,b are_connected by BORSUK_2:def 3;
A2: b,c are_connected by BORSUK_2:def 3;
A3: c,d are_connected by BORSUK_2:def 3;
A4: d,e are_connected by BORSUK_2:def 3;
e,z are_connected by BORSUK_2:def 3;
hence rng ((((f + g) + h) + i) + j) = ((((rng f) \/ (rng g)) \/ (rng h)) \/ (rng i)) \/ (rng j) by A1, A2, A3, A4, Lm10; :: thesis: verum