let n be Element of NAT ; :: thesis: for P1, P2 being Subset of (TOP-REAL n)
for p1, p2 being Point of (TOP-REAL n) st P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & P1 c= P2 holds
P1 = P2
let P1, P2 be Subset of (TOP-REAL n); :: thesis: for p1, p2 being Point of (TOP-REAL n) st P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & P1 c= P2 holds
P1 = P2
let p1, p2 be Point of (TOP-REAL n); :: thesis: ( P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & P1 c= P2 implies P1 = P2 )
assume A1:
( P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & P1 c= P2 )
; :: thesis: P1 = P2
then reconsider P1' = P1, P2' = P2 as non empty Subset of (TOP-REAL n) by TOPREAL1:4;
now assume A2:
P2 \ P1 <> {}
;
:: thesis: contradictionconsider p being
Element of
P2 \ P1;
A3:
(
p in P2 & not
p in P1 )
by A2, XBOOLE_0:def 5;
consider f1 being
Function of
I[01] ,
((TOP-REAL n) | P1') such that A4:
(
f1 is
being_homeomorphism &
f1 . 0 = p1 &
f1 . 1
= p2 )
by A1, TOPREAL1:def 2;
A5:
f1 is
continuous
by A4, TOPS_2:def 5;
consider f2 being
Function of
I[01] ,
((TOP-REAL n) | P2') such that A6:
(
f2 is
being_homeomorphism &
f2 . 0 = p1 &
f2 . 1
= p2 )
by A1, TOPREAL1:def 2;
reconsider f4 =
f2 as
Function ;
A7:
f2 is
one-to-one
by A6, TOPS_2:def 5;
A8:
(
dom f2 = [#] I[01] &
rng f2 = [#] ((TOP-REAL n) | P2) )
by A6, TOPS_2:def 5;
A9:
f2 " is
being_homeomorphism
by A6, TOPS_2:70;
then A10:
dom (f2 " ) =
[#] ((TOP-REAL n) | P2)
by TOPS_2:def 5
.=
P2
by PRE_TOPC:def 10
;
f2 " is
continuous
by A6, TOPS_2:def 5;
then consider h being
Function of
I[01] ,
I[01] such that A11:
(
h = (f2 " ) * f1 &
h is
continuous )
by A1, A5, Th58;
reconsider h1 =
h as
Function of
(Closed-Interval-TSpace 0 ,1),
R^1 by BORSUK_1:83, FUNCT_2:9, TOPMETR:24, TOPMETR:27;
h1 is
continuous
then reconsider g =
h1 as
continuous Function of
(Closed-Interval-TSpace 0 ,1),
R^1 ;
A15:
dom f1 =
[#] I[01]
by A4, TOPS_2:def 5
.=
[.0 ,1.]
by BORSUK_1:83
;
then A16:
0 in dom f1
by XXREAL_1:1;
A17:
1
in dom f1
by A15, XXREAL_1:1;
A18:
g . 0 = (f2 " ) . p1
by A4, A11, A16, FUNCT_1:23;
A19:
g . 1
= (f2 " ) . p2
by A4, A11, A17, FUNCT_1:23;
A20:
dom f2 =
[#] I[01]
by A6, TOPS_2:def 5
.=
[.0 ,1.]
by BORSUK_1:83
;
then A21:
0 in dom f2
by XXREAL_1:1;
A22:
1
in dom f2
by A20, XXREAL_1:1;
A23:
(f2 " ) . p1 = (f4 " ) . p1
by A7, A8, TOPS_2:def 4;
(f2 " ) . p2 = (f4 " ) . p2
by A7, A8, TOPS_2:def 4;
then A24:
(
g . 0 = 0 &
g . 1
= 1 )
by A6, A7, A18, A19, A21, A22, A23, FUNCT_1:54;
p in the
carrier of
((TOP-REAL n) | P2')
by A3, PRE_TOPC:29;
then A25:
(f2 " ) . p in the
carrier of
I[01]
by FUNCT_2:7;
A26:
now assume
(f2 " ) . p in rng g
;
:: thesis: contradictionthen consider x being
set such that A27:
(
x in dom g &
(f2 " ) . p = g . x )
by FUNCT_1:def 5;
A28:
(f2 " ) . p = (f2 " ) . (f1 . x)
by A11, A27, FUNCT_1:22;
A29:
(
x in dom f1 &
f1 . x in dom (f2 " ) )
by A11, A27, FUNCT_1:21;
f2 " is
one-to-one
by A9, TOPS_2:def 5;
then
p = f1 . x
by A3, A10, A28, A29, FUNCT_1:def 8;
then A30:
p in rng f1
by A29, FUNCT_1:def 5;
rng f1 =
[#] ((TOP-REAL n) | P1)
by A4, TOPS_2:def 5
.=
P1
by PRE_TOPC:def 10
;
hence
contradiction
by A2, A30, XBOOLE_0:def 5;
:: thesis: verum end; reconsider r =
(f2 " ) . p as
Real by A25, BORSUK_1:83;
A31:
rng f2 =
[#] ((TOP-REAL n) | P2)
by A6, TOPS_2:def 5
.=
P2
by PRE_TOPC:def 10
;
A32:
(
0 <= r &
r <= 1 )
by A25, BORSUK_1:83, XXREAL_1:1;
then
(
0 < r &
r < 1 )
by A32, A33, XXREAL_0:1;
then consider rc being
Real such that A36:
(
g . rc = r &
0 < rc &
rc < 1 )
by A24, TOPREAL5:12;
the
carrier of
((TOP-REAL n) | P1) =
[#] ((TOP-REAL n) | P1)
.=
P1
by PRE_TOPC:def 10
;
then
rng f1 c= dom (f2 " )
by A1, A10, XBOOLE_1:1;
then dom g =
dom f1
by A11, RELAT_1:46
.=
[#] I[01]
by A4, TOPS_2:def 5
.=
[.0 ,1.]
by BORSUK_1:83
;
then
rc in dom g
by A36, XXREAL_1:1;
hence
contradiction
by A26, A36, FUNCT_1:def 5;
:: thesis: verum end;
then
P2 c= P1
by XBOOLE_1:37;
hence
P1 = P2
by A1, XBOOLE_0:def 10; :: thesis: verum