let n be Nat; for P being Subset of (TOP-REAL n)
for w1, w2, w3 being Point of (TOP-REAL n) st w1 in P & w2 in P & w3 in P & LSeg (w1,w2) c= P & LSeg (w2,w3) c= P holds
ex h being Function of I[01],((TOP-REAL n) | P) st
( h is continuous & w1 = h . 0 & w3 = h . 1 )
let P be Subset of (TOP-REAL n); for w1, w2, w3 being Point of (TOP-REAL n) st w1 in P & w2 in P & w3 in P & LSeg (w1,w2) c= P & LSeg (w2,w3) c= P holds
ex h being Function of I[01],((TOP-REAL n) | P) st
( h is continuous & w1 = h . 0 & w3 = h . 1 )
let w1, w2, w3 be Point of (TOP-REAL n); ( w1 in P & w2 in P & w3 in P & LSeg (w1,w2) c= P & LSeg (w2,w3) c= P implies ex h being Function of I[01],((TOP-REAL n) | P) st
( h is continuous & w1 = h . 0 & w3 = h . 1 ) )
assume that
A1:
w1 in P
and
A2:
w2 in P
and
A3:
w3 in P
and
A4:
LSeg (w1,w2) c= P
and
A5:
LSeg (w2,w3) c= P
; ex h being Function of I[01],((TOP-REAL n) | P) st
( h is continuous & w1 = h . 0 & w3 = h . 1 )
reconsider Y = P as non empty Subset of (TOP-REAL n) by A1;
per cases
( w1 <> w2 or w1 = w2 )
;
suppose A6:
w1 <> w2
;
ex h being Function of I[01],((TOP-REAL n) | P) st
( h is continuous & w1 = h . 0 & w3 = h . 1 )then
LSeg (
w1,
w2)
is_an_arc_of w1,
w2
by TOPREAL1:9;
then consider f being
Function of
I[01],
((TOP-REAL n) | (LSeg (w1,w2))) such that A7:
f is
being_homeomorphism
and A8:
f . 0 = w1
and A9:
f . 1
= w2
by TOPREAL1:def 1;
A10:
rng f = [#] ((TOP-REAL n) | (LSeg (w1,w2)))
by A7;
then A11:
rng f c= P
by A4, PRE_TOPC:def 5;
then
[#] ((TOP-REAL n) | (LSeg (w1,w2))) c= [#] ((TOP-REAL n) | P)
by A10, PRE_TOPC:def 5;
then A12:
(TOP-REAL n) | (LSeg (w1,w2)) is
SubSpace of
(TOP-REAL n) | P
by TOPMETR:3;
dom f = [.0,1.]
by BORSUK_1:40, FUNCT_2:def 1;
then reconsider g =
f as
Function of
[.0,1.],
P by A11, FUNCT_2:2;
reconsider gt =
g as
Function of
I[01],
((TOP-REAL n) | Y) by BORSUK_1:40, PRE_TOPC:8;
A13:
f is
continuous
by A7;
now ex h being Function of I[01],((TOP-REAL n) | P) st
( h is continuous & w1 = h . 0 & w3 = h . 1 )per cases
( w2 <> w3 or w2 = w3 )
;
suppose
w2 <> w3
;
ex h being Function of I[01],((TOP-REAL n) | P) st
( h is continuous & w1 = h . 0 & w3 = h . 1 )then
LSeg (
w2,
w3)
is_an_arc_of w2,
w3
by TOPREAL1:9;
then consider f2 being
Function of
I[01],
((TOP-REAL n) | (LSeg (w2,w3))) such that A14:
f2 is
being_homeomorphism
and A15:
(
f2 . 0 = w2 &
f2 . 1
= w3 )
by TOPREAL1:def 1;
A16:
rng f2 = [#] ((TOP-REAL n) | (LSeg (w2,w3)))
by A14;
then A17:
rng f2 c= P
by A5, PRE_TOPC:def 5;
then
[#] ((TOP-REAL n) | (LSeg (w2,w3))) c= [#] ((TOP-REAL n) | P)
by A16, PRE_TOPC:def 5;
then A18:
(TOP-REAL n) | (LSeg (w2,w3)) is
SubSpace of
(TOP-REAL n) | P
by TOPMETR:3;
[#] ((TOP-REAL n) | P) = P
by PRE_TOPC:def 5;
then reconsider w19 =
w1,
w29 =
w2,
w39 =
w3 as
Point of
((TOP-REAL n) | P) by A1, A2, A3;
A19:
(
gt is
continuous &
w29 = gt . 1 )
by A9, A13, A12, PRE_TOPC:26;
dom f2 = [.0,1.]
by BORSUK_1:40, FUNCT_2:def 1;
then reconsider g2 =
f2 as
Function of
[.0,1.],
P by A17, FUNCT_2:2;
reconsider gt2 =
g2 as
Function of
I[01],
((TOP-REAL n) | Y) by BORSUK_1:40, PRE_TOPC:8;
f2 is
continuous
by A14;
then
gt2 is
continuous
by A18, PRE_TOPC:26;
then
ex
h being
Function of
I[01],
((TOP-REAL n) | Y) st
(
h is
continuous &
w19 = h . 0 &
w39 = h . 1 &
rng h c= (rng gt) \/ (rng gt2) )
by A8, A15, A19, BORSUK_2:13;
hence
ex
h being
Function of
I[01],
((TOP-REAL n) | P) st
(
h is
continuous &
w1 = h . 0 &
w3 = h . 1 )
;
verum end; suppose A20:
w2 = w3
;
ex h being Function of I[01],((TOP-REAL n) | P) st
( h is continuous & w1 = h . 0 & w3 = h . 1 )then
LSeg (
w1,
w3)
is_an_arc_of w1,
w3
by A6, TOPREAL1:9;
then consider f being
Function of
I[01],
((TOP-REAL n) | (LSeg (w1,w3))) such that A21:
f is
being_homeomorphism
and A22:
(
f . 0 = w1 &
f . 1
= w3 )
by TOPREAL1:def 1;
A23:
rng f = [#] ((TOP-REAL n) | (LSeg (w1,w3)))
by A21;
then A24:
rng f c= P
by A4, A20, PRE_TOPC:def 5;
then
[#] ((TOP-REAL n) | (LSeg (w1,w3))) c= [#] ((TOP-REAL n) | P)
by A23, PRE_TOPC:def 5;
then A25:
(TOP-REAL n) | (LSeg (w1,w3)) is
SubSpace of
(TOP-REAL n) | P
by TOPMETR:3;
dom f = [.0,1.]
by BORSUK_1:40, FUNCT_2:def 1;
then reconsider g =
f as
Function of
[.0,1.],
P by A24, FUNCT_2:2;
reconsider gt =
g as
Function of
I[01],
((TOP-REAL n) | Y) by BORSUK_1:40, PRE_TOPC:8;
f is
continuous
by A21;
then
gt is
continuous
by A25, PRE_TOPC:26;
hence
ex
h being
Function of
I[01],
((TOP-REAL n) | P) st
(
h is
continuous &
w1 = h . 0 &
w3 = h . 1 )
by A22;
verum end; hence
ex
h being
Function of
I[01],
((TOP-REAL n) | P) st
(
h is
continuous &
w1 = h . 0 &
w3 = h . 1 )
;
verum end; suppose A26:
w1 = w2
;
ex h being Function of I[01],((TOP-REAL n) | P) st
( h is continuous & w1 = h . 0 & w3 = h . 1 )now ( ( w2 <> w3 & ex h being Function of I[01],((TOP-REAL n) | P) st
( h is continuous & w1 = h . 0 & w3 = h . 1 ) ) or ( w2 = w3 & ex h being Function of I[01],((TOP-REAL n) | P) st
( h is continuous & w1 = h . 0 & w3 = h . 1 ) ) )per cases
( w2 <> w3 or w2 = w3 )
;
case
w2 <> w3
;
ex h being Function of I[01],((TOP-REAL n) | P) st
( h is continuous & w1 = h . 0 & w3 = h . 1 )then
LSeg (
w1,
w3)
is_an_arc_of w1,
w3
by A26, TOPREAL1:9;
then consider f being
Function of
I[01],
((TOP-REAL n) | (LSeg (w1,w3))) such that A27:
f is
being_homeomorphism
and A28:
(
f . 0 = w1 &
f . 1
= w3 )
by TOPREAL1:def 1;
A29:
rng f = [#] ((TOP-REAL n) | (LSeg (w1,w3)))
by A27;
then A30:
rng f c= P
by A5, A26, PRE_TOPC:def 5;
then
[#] ((TOP-REAL n) | (LSeg (w1,w3))) c= [#] ((TOP-REAL n) | P)
by A29, PRE_TOPC:def 5;
then A31:
(TOP-REAL n) | (LSeg (w1,w3)) is
SubSpace of
(TOP-REAL n) | P
by TOPMETR:3;
dom f = [.0,1.]
by BORSUK_1:40, FUNCT_2:def 1;
then reconsider g =
f as
Function of
[.0,1.],
P by A30, FUNCT_2:2;
reconsider gt =
g as
Function of
I[01],
((TOP-REAL n) | Y) by BORSUK_1:40, PRE_TOPC:8;
f is
continuous
by A27;
then
gt is
continuous
by A31, PRE_TOPC:26;
hence
ex
h being
Function of
I[01],
((TOP-REAL n) | P) st
(
h is
continuous &
w1 = h . 0 &
w3 = h . 1 )
by A28;
verum end; hence
ex
h being
Function of
I[01],
((TOP-REAL n) | P) st
(
h is
continuous &
w1 = h . 0 &
w3 = h . 1 )
;
verum