let n be Element of 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, Th44;
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:15;
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 2;
A11:
rng f = [#] ((TOP-REAL n) | (LSeg w3,w4))
by A9, TOPS_2:def 5;
then A12:
rng f c= P
by A6, PRE_TOPC:def 10;
then
[#] ((TOP-REAL n) | (LSeg w3,w4)) c= [#] ((TOP-REAL n) | P)
by A11, PRE_TOPC:def 10;
then A13:
(TOP-REAL n) | (LSeg w3,w4) is
SubSpace of
(TOP-REAL n) | P
by TOPMETR:4;
[#] ((TOP-REAL n) | P) = P
by PRE_TOPC:def 10;
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:83, FUNCT_2:def 1;
then reconsider g =
f as
Function of
[.0 ,1.],
P by A12, FUNCT_2:4;
reconsider gt =
g as
Function of
I[01] ,
((TOP-REAL n) | Y) by BORSUK_1:83, PRE_TOPC:29;
f is
continuous
by A9, TOPS_2:def 5;
then
gt is
continuous
by A13, PRE_TOPC:56;
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:16;
hence
ex
h being
Function of
I[01] ,
((TOP-REAL n) | P) st
(
h is
continuous &
w1 = h . 0 &
w4 = h . 1 )
;
verum end;