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