let T be non empty TopSpace; 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; 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; 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; ( 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
; rng f c= rng (g + f)
let y be object ; TARSKI:def 3 ( not y in rng f or y in rng (g + f) )
assume
y in rng f
; 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; verum