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