let T be non empty pathwise_connected TopSpace; for a, b, c being Point of T
for f being Path of a,b
for g being Path of b,c holds rng f c= rng (f + g)
let a, b, c be Point of T; for f being Path of a,b
for g being Path of b,c holds rng f c= rng (f + g)
let f be Path of a,b; for g being Path of b,c holds rng f c= rng (f + g)
let g be Path of b,c; rng f c= rng (f + g)
A1:
a,b are_connected
by BORSUK_2:def 3;
b,c are_connected
by BORSUK_2:def 3;
hence
rng f c= rng (f + g)
by A1, Th33; verum