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