let T be non empty 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 st a,b are_connected & b,c are_connected & c,d are_connected & d,e are_connected & e,z are_connected 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 st a,b are_connected & b,c are_connected & c,d are_connected & d,e are_connected & e,z are_connected 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 st a,b are_connected & b,c are_connected & c,d are_connected & d,e are_connected & e,z are_connected 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 st a,b are_connected & b,c are_connected & c,d are_connected & d,e are_connected & e,z are_connected 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 st a,b are_connected & b,c are_connected & c,d are_connected & d,e are_connected & e,z are_connected 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 st a,b are_connected & b,c are_connected & c,d are_connected & d,e are_connected & e,z are_connected 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: ( a,b are_connected & b,c are_connected & c,d are_connected & d,e are_connected & e,z are_connected implies rng ((((f + g) + h) + i) + j) = ((((rng f) \/ (rng g)) \/ (rng h)) \/ (rng i)) \/ (rng j) )
assume that
A1: a,b are_connected and
A2: b,c are_connected and
A3: c,d are_connected and
A4: d,e are_connected and
A5: e,z are_connected ; :: thesis: rng ((((f + g) + h) + i) + j) = ((((rng f) \/ (rng g)) \/ (rng h)) \/ (rng i)) \/ (rng j)
a,c are_connected by A1, A2, BORSUK_6:42;
then a,d are_connected by A3, BORSUK_6:42;
then a,e are_connected by A4, BORSUK_6:42;
hence rng ((((f + g) + h) + i) + j) = (rng (((f + g) + h) + i)) \/ (rng j) by A5, Th37
.= ((((rng f) \/ (rng g)) \/ (rng h)) \/ (rng i)) \/ (rng j) by A1, A2, A3, A4, Lm8 ;
:: thesis: verum