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