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