let n be Nat; for P being Subset of (TOP-REAL n)
for w1, w2, w3, w4 being Point of (TOP-REAL n) st w1 in P & w2 in P & w3 in P & w4 in P & LSeg (w1,w2) c= P & LSeg (w2,w3) c= P & LSeg (w3,w4) c= P holds
ex h being Function of I[01],((TOP-REAL n) | P) st
( h is continuous & w1 = h . 0 & w4 = h . 1 )
let P be Subset of (TOP-REAL n); for w1, w2, w3, w4 being Point of (TOP-REAL n) st w1 in P & w2 in P & w3 in P & w4 in P & LSeg (w1,w2) c= P & LSeg (w2,w3) c= P & LSeg (w3,w4) c= P holds
ex h being Function of I[01],((TOP-REAL n) | P) st
( h is continuous & w1 = h . 0 & w4 = h . 1 )
let w1, w2, w3, w4 be Point of (TOP-REAL n); ( w1 in P & w2 in P & w3 in P & w4 in P & LSeg (w1,w2) c= P & LSeg (w2,w3) c= P & LSeg (w3,w4) c= P implies ex h being Function of I[01],((TOP-REAL n) | P) st
( h is continuous & w1 = h . 0 & w4 = h . 1 ) )
assume that
A1:
w1 in P
and
A2:
w2 in P
and
A3:
w3 in P
and
A4:
w4 in P
and
A5:
( LSeg (w1,w2) c= P & LSeg (w2,w3) c= P )
and
A6:
LSeg (w3,w4) c= P
; ex h being Function of I[01],((TOP-REAL n) | P) st
( h is continuous & w1 = h . 0 & w4 = h . 1 )
reconsider Y = P as non empty Subset of (TOP-REAL n) by A1;
consider h2 being Function of I[01],((TOP-REAL n) | P) such that
A7:
( h2 is continuous & w1 = h2 . 0 )
and
A8:
w3 = h2 . 1
by A1, A2, A3, A5, Th25;
per cases
( w3 <> w4 or w3 = w4 )
;
suppose
w3 <> w4
;
ex h being Function of I[01],((TOP-REAL n) | P) st
( h is continuous & w1 = h . 0 & w4 = h . 1 )then
LSeg (
w3,
w4)
is_an_arc_of w3,
w4
by TOPREAL1:9;
then consider f being
Function of
I[01],
((TOP-REAL n) | (LSeg (w3,w4))) such that A9:
f is
being_homeomorphism
and A10:
(
f . 0 = w3 &
f . 1
= w4 )
by TOPREAL1:def 1;
A11:
rng f = [#] ((TOP-REAL n) | (LSeg (w3,w4)))
by A9;
then A12:
rng f c= P
by A6, PRE_TOPC:def 5;
then
[#] ((TOP-REAL n) | (LSeg (w3,w4))) c= [#] ((TOP-REAL n) | P)
by A11, PRE_TOPC:def 5;
then A13:
(TOP-REAL n) | (LSeg (w3,w4)) is
SubSpace of
(TOP-REAL n) | P
by TOPMETR:3;
[#] ((TOP-REAL n) | P) = P
by PRE_TOPC:def 5;
then reconsider w19 =
w1,
w39 =
w3,
w49 =
w4 as
Point of
((TOP-REAL n) | P) by A1, A3, A4;
A14:
w39 = h2 . 1
by A8;
dom f = [.0,1.]
by BORSUK_1:40, FUNCT_2:def 1;
then reconsider g =
f as
Function of
[.0,1.],
P by A12, 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 A9;
then
gt is
continuous
by A13, PRE_TOPC:26;
then
ex
h being
Function of
I[01],
((TOP-REAL n) | Y) st
(
h is
continuous &
w19 = h . 0 &
w49 = h . 1 &
rng h c= (rng h2) \/ (rng gt) )
by A7, A10, A14, BORSUK_2:13;
hence
ex
h being
Function of
I[01],
((TOP-REAL n) | P) st
(
h is
continuous &
w1 = h . 0 &
w4 = h . 1 )
;
verum end;