let T be non empty TopSpace; :: thesis: for a, b, c being Point of T
for f being Path of b,c
for g being Path of a,b st a,b are_connected & b,c are_connected 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 st a,b are_connected & b,c are_connected holds
rng f c= rng (g + f)
let f be Path of b,c; :: thesis: for g being Path of a,b st a,b are_connected & b,c are_connected holds
rng f c= rng (g + f)
let g be Path of a,b; :: thesis: ( a,b are_connected & b,c are_connected implies rng f c= rng (g + f) )
assume that
A1: a,b are_connected and
A2: b,c are_connected ; :: thesis: rng f c= rng (g + f)
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f or y in rng (g + f) )
assume y in rng f ; :: thesis: y in rng (g + f)
then consider x being object such that
A3: x in dom f and
A4: f . x = y by FUNCT_1:def 3;
A5: dom (g + f) = the carrier of I[01] by FUNCT_2:def 1;
reconsider x = x as Point of I[01] by A3;
A6: 0 <= x by BORSUK_1:43;
then A7: 0 + (1 / 2) <= (x / 2) + (1 / 2) by XREAL_1:6;
x <= 1 by BORSUK_1:43;
then x + 1 <= 1 + 1 by XREAL_1:6;
then (x + 1) / 2 <= 2 / 2 by XREAL_1:72;
then A8: (x / 2) + (1 / 2) is Point of I[01] by A6, BORSUK_1:43;
then (g + f) . ((x / 2) + (1 / 2)) = f . ((2 * ((x / 2) + (1 / 2))) - 1) by A1, A2, A7, BORSUK_2:def 5;
hence y in rng (g + f) by A4, A5, A8, FUNCT_1:def 3; :: thesis: verum