let n be Element of NAT ; :: thesis: 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); :: thesis: 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); :: thesis: ( 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 A1:
( 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 )
; :: thesis: ex h being Function of I[01] ,((TOP-REAL n) | P) st
( h is continuous & w1 = h . 0 & w4 = h . 1 )
then consider h2 being Function of I[01] ,((TOP-REAL n) | P) such that
A2:
( h2 is continuous & w1 = h2 . 0 & w3 = h2 . 1 )
by Th44;
reconsider Y = P as non empty Subset of (TOP-REAL n) by A1;
per cases
( w3 <> w4 or w3 = w4 )
;
suppose
w3 <> w4
;
:: thesis: 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 A3:
(
f is
being_homeomorphism &
f . 0 = w3 &
f . 1
= w4 )
by TOPREAL1:def 2;
A4:
f is
continuous
by A3, TOPS_2:def 5;
A5:
rng f = [#] ((TOP-REAL n) | (LSeg w3,w4))
by A3, TOPS_2:def 5;
then A6:
rng f c= P
by A1, PRE_TOPC:def 10;
then
[#] ((TOP-REAL n) | (LSeg w3,w4)) c= [#] ((TOP-REAL n) | P)
by A5, PRE_TOPC:def 10;
then A7:
(TOP-REAL n) | (LSeg w3,w4) is
SubSpace of
(TOP-REAL n) | P
by TOPMETR:4;
dom f = [.0 ,1.]
by BORSUK_1:83, FUNCT_2:def 1;
then reconsider g =
f as
Function of
[.0 ,1.],
P by A6, FUNCT_2:4;
the
carrier of
((TOP-REAL n) | P) = P
by PRE_TOPC:29;
then reconsider gt =
g as
Function of
I[01] ,
((TOP-REAL n) | Y) by BORSUK_1:83;
A8:
gt is
continuous
by A4, A7, PRE_TOPC:56;
[#] ((TOP-REAL n) | P) = P
by PRE_TOPC:def 10;
then reconsider w1' =
w1,
w3' =
w3,
w4' =
w4 as
Point of
((TOP-REAL n) | P) by A1;
(
h2 is
continuous &
w1' = h2 . 0 &
w3' = h2 . 1 )
by A2;
then
ex
h being
Function of
I[01] ,
((TOP-REAL n) | Y) st
(
h is
continuous &
w1' = h . 0 &
w4' = h . 1 &
rng h c= (rng h2) \/ (rng gt) )
by A3, A8, 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 )
;
:: thesis: verum end;