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 + g) = (rng f) \/ (rng 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 + g) = (rng f) \/ (rng 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 + g) = (rng f) \/ (rng g)
let g be Path of b,c; :: thesis: ( a,b are_connected & b,c are_connected implies rng (f + g) = (rng f) \/ (rng g) )
assume that
A1: a,b are_connected and
A2: b,c are_connected ; :: thesis: rng (f + g) = (rng f) \/ (rng g)
thus rng (f + g) c= (rng f) \/ (rng g) :: according to XBOOLE_0:def 10 :: thesis: (rng f) \/ (rng g) c= rng (f + g)
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (f + g) or y in (rng f) \/ (rng g) )
assume y in rng (f + g) ; :: thesis: y in (rng f) \/ (rng g)
then consider x being object such that
A3: x in dom (f + g) and
A4: y = (f + g) . x by FUNCT_1:def 3;
reconsider x = x as Point of I[01] by A3;
per cases ( x <= 1 / 2 or 1 / 2 <= x ) ;
suppose A5: x <= 1 / 2 ; :: thesis: y in (rng f) \/ (rng g)
then A6: (f + g) . x = f . (2 * x) by A1, A2, BORSUK_2:def 5;
A7: rng f c= (rng f) \/ (rng g) by XBOOLE_1:7;
A8: dom f = the carrier of I[01] by FUNCT_2:def 1;
2 * x is Point of I[01] by A5, BORSUK_6:3;
then y in rng f by A4, A6, A8, FUNCT_1:def 3;
hence y in (rng f) \/ (rng g) by A7; :: thesis: verum
end;
suppose A9: 1 / 2 <= x ; :: thesis: y in (rng f) \/ (rng g)
then A10: (f + g) . x = g . ((2 * x) - 1) by A1, A2, BORSUK_2:def 5;
A11: rng g c= (rng f) \/ (rng g) by XBOOLE_1:7;
A12: dom g = the carrier of I[01] by FUNCT_2:def 1;
(2 * x) - 1 is Point of I[01] by A9, BORSUK_6:4;
then y in rng g by A4, A10, A12, FUNCT_1:def 3;
hence y in (rng f) \/ (rng g) by A11; :: thesis: verum
end;
end;
end;
A13: rng f c= rng (f + g) by A1, A2, Th33;
rng g c= rng (f + g) by A1, A2, Th35;
hence (rng f) \/ (rng g) c= rng (f + g) by A13, XBOOLE_1:8; :: thesis: verum