let n be Element of NAT ; :: thesis: 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); :: thesis: 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); :: thesis: ( 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 A1:
( w1 in P & w2 in P & w3 in P & LSeg w1,w2 c= P & LSeg w2,w3 c= P )
; :: thesis: ex h being Function of I[01] ,((TOP-REAL n) | P) st
( h is continuous & w1 = h . 0 & w3 = h . 1 )
then reconsider Y = P as non empty Subset of (TOP-REAL n) ;
per cases
( w1 <> w2 or w1 = w2 )
;
suppose A2:
w1 <> w2
;
:: thesis: 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:15;
then consider f being
Function of
I[01] ,
((TOP-REAL n) | (LSeg w1,w2)) such that A3:
(
f is
being_homeomorphism &
f . 0 = w1 &
f . 1
= w2 )
by TOPREAL1:def 2;
A4:
f is
continuous
by A3, TOPS_2:def 5;
A5:
rng f = [#] ((TOP-REAL n) | (LSeg w1,w2))
by A3, TOPS_2:def 5;
then A6:
rng f c= P
by A1, PRE_TOPC:def 10;
then
[#] ((TOP-REAL n) | (LSeg w1,w2)) c= [#] ((TOP-REAL n) | P)
by A5, PRE_TOPC:def 10;
then A7:
(TOP-REAL n) | (LSeg w1,w2) 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;
now per cases
( w2 <> w3 or w2 = w3 )
;
suppose
w2 <> w3
;
:: thesis: 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:15;
then consider f2 being
Function of
I[01] ,
((TOP-REAL n) | (LSeg w2,w3)) such that A8:
(
f2 is
being_homeomorphism &
f2 . 0 = w2 &
f2 . 1
= w3 )
by TOPREAL1:def 2;
A9:
f2 is
continuous
by A8, TOPS_2:def 5;
A10:
rng f2 = [#] ((TOP-REAL n) | (LSeg w2,w3))
by A8, TOPS_2:def 5;
then A11:
rng f2 c= P
by A1, PRE_TOPC:def 10;
then
[#] ((TOP-REAL n) | (LSeg w2,w3)) c= [#] ((TOP-REAL n) | P)
by A10, PRE_TOPC:def 10;
then A12:
(TOP-REAL n) | (LSeg w2,w3) is
SubSpace of
(TOP-REAL n) | P
by TOPMETR:4;
dom f2 = [.0 ,1.]
by BORSUK_1:83, FUNCT_2:def 1;
then reconsider g2 =
f2 as
Function of
[.0 ,1.],
P by A11, FUNCT_2:4;
the
carrier of
((TOP-REAL n) | P) = P
by PRE_TOPC:29;
then reconsider gt2 =
g2 as
Function of
I[01] ,
((TOP-REAL n) | Y) by BORSUK_1:83;
A13:
gt2 is
continuous
by A9, A12, PRE_TOPC:56;
[#] ((TOP-REAL n) | P) = P
by PRE_TOPC:def 10;
then reconsider w1' =
w1,
w2' =
w2,
w3' =
w3 as
Point of
((TOP-REAL n) | P) by A1;
(
gt is
continuous &
w1' = gt . 0 &
w2' = gt . 1 )
by A3, A4, A7, PRE_TOPC:56;
then
ex
h being
Function of
I[01] ,
((TOP-REAL n) | Y) st
(
h is
continuous &
w1' = h . 0 &
w3' = h . 1 &
rng h c= (rng gt) \/ (rng gt2) )
by A8, A13, BORSUK_2:16;
hence
ex
h being
Function of
I[01] ,
((TOP-REAL n) | P) st
(
h is
continuous &
w1 = h . 0 &
w3 = h . 1 )
;
:: thesis: verum end; suppose A14:
w2 = w3
;
:: thesis: 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 A2, TOPREAL1:15;
then consider f being
Function of
I[01] ,
((TOP-REAL n) | (LSeg w1,w3)) such that A15:
(
f is
being_homeomorphism &
f . 0 = w1 &
f . 1
= w3 )
by TOPREAL1:def 2;
A16:
f is
continuous
by A15, TOPS_2:def 5;
A17:
rng f = [#] ((TOP-REAL n) | (LSeg w1,w3))
by A15, TOPS_2:def 5;
then A18:
rng f c= P
by A1, A14, PRE_TOPC:def 10;
then
[#] ((TOP-REAL n) | (LSeg w1,w3)) c= [#] ((TOP-REAL n) | P)
by A17, PRE_TOPC:def 10;
then A19:
(TOP-REAL n) | (LSeg w1,w3) 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 A18, 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;
gt is
continuous
by A16, A19, PRE_TOPC:56;
hence
ex
h being
Function of
I[01] ,
((TOP-REAL n) | P) st
(
h is
continuous &
w1 = h . 0 &
w3 = h . 1 )
by A15;
:: thesis: verum end; hence
ex
h being
Function of
I[01] ,
((TOP-REAL n) | P) st
(
h is
continuous &
w1 = h . 0 &
w3 = h . 1 )
;
:: thesis: verum end; suppose A20:
w1 = w2
;
:: thesis: ex h being Function of I[01] ,((TOP-REAL n) | P) st
( h is continuous & w1 = h . 0 & w3 = h . 1 )now per cases
( w2 <> w3 or w2 = w3 )
;
case
w2 <> w3
;
:: thesis: 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 A20, TOPREAL1:15;
then consider f being
Function of
I[01] ,
((TOP-REAL n) | (LSeg w1,w3)) such that A21:
(
f is
being_homeomorphism &
f . 0 = w1 &
f . 1
= w3 )
by TOPREAL1:def 2;
A22:
f is
continuous
by A21, TOPS_2:def 5;
A23:
rng f = [#] ((TOP-REAL n) | (LSeg w1,w3))
by A21, TOPS_2:def 5;
then A24:
rng f c= P
by A1, A20, PRE_TOPC:def 10;
then
[#] ((TOP-REAL n) | (LSeg w1,w3)) c= [#] ((TOP-REAL n) | P)
by A23, PRE_TOPC:def 10;
then A25:
(TOP-REAL n) | (LSeg w1,w3) 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 A24, 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;
gt is
continuous
by A22, A25, PRE_TOPC:56;
hence
ex
h being
Function of
I[01] ,
((TOP-REAL n) | P) st
(
h is
continuous &
w1 = h . 0 &
w3 = h . 1 )
by A21;
:: thesis: verum end; hence
ex
h being
Function of
I[01] ,
((TOP-REAL n) | P) st
(
h is
continuous &
w1 = h . 0 &
w3 = h . 1 )
;
:: thesis: verum