let n be 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 that

A1: P1 is_an_arc_of p1,p2 and

A2: P2 is_an_arc_of p1,p2 and

A3: P1 c= P2 ; :: thesis: P1 = P2

reconsider P19 = P1, P29 = P2 as non empty Subset of (TOP-REAL n) by A1, A2, TOPREAL1:1;

hence P1 = P2 by A3; :: thesis: verum

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 that

A1: P1 is_an_arc_of p1,p2 and

A2: P2 is_an_arc_of p1,p2 and

A3: P1 c= P2 ; :: thesis: P1 = P2

reconsider P19 = P1, P29 = P2 as non empty Subset of (TOP-REAL n) by A1, A2, TOPREAL1:1;

now :: thesis: not P2 \ P1 <> {}

then
P2 c= P1
by XBOOLE_1:37;assume A4:
P2 \ P1 <> {}
; :: thesis: contradiction

set p = the Element of P2 \ P1;

A5: the Element of P2 \ P1 in P2 by A4, XBOOLE_0:def 5;

A6: not the Element of P2 \ P1 in P1 by A4, XBOOLE_0:def 5;

consider f1 being Function of I[01],((TOP-REAL n) | P19) such that

A7: f1 is being_homeomorphism and

A8: f1 . 0 = p1 and

A9: f1 . 1 = p2 by A1, TOPREAL1:def 1;

A10: f1 is continuous by A7, TOPS_2:def 5;

consider f2 being Function of I[01],((TOP-REAL n) | P29) such that

A11: f2 is being_homeomorphism and

A12: f2 . 0 = p1 and

A13: f2 . 1 = p2 by A2, TOPREAL1:def 1;

reconsider f4 = f2 as Function ;

A14: f2 is one-to-one by A11, TOPS_2:def 5;

A15: rng f2 = [#] ((TOP-REAL n) | P2) by A11, TOPS_2:def 5;

A16: f2 " is being_homeomorphism by A11, TOPS_2:56;

then A17: dom (f2 ") = [#] ((TOP-REAL n) | P2) by TOPS_2:def 5

.= P2 by PRE_TOPC:def 5 ;

f2 " is continuous by A11, TOPS_2:def 5;

then consider h being Function of I[01],I[01] such that

A18: h = (f2 ") * f1 and

A19: h is continuous by A3, A10, Th45;

reconsider h1 = h as Function of (Closed-Interval-TSpace (0,1)),R^1 by BORSUK_1:40, FUNCT_2:7, TOPMETR:17, TOPMETR:20;

for F1 being Subset of R^1 st F1 is closed holds

h1 " F1 is closed

A23: dom f1 = [#] I[01] by A7, TOPS_2:def 5

.= [.0,1.] by BORSUK_1:40 ;

then A24: 0 in dom f1 by XXREAL_1:1;

A25: 1 in dom f1 by A23, XXREAL_1:1;

A26: g . 0 = (f2 ") . p1 by A8, A18, A24, FUNCT_1:13;

A27: g . 1 = (f2 ") . p2 by A9, A18, A25, FUNCT_1:13;

A28: dom f2 = [#] I[01] by A11, TOPS_2:def 5

.= [.0,1.] by BORSUK_1:40 ;

then A29: 0 in dom f2 by XXREAL_1:1;

A30: 1 in dom f2 by A28, XXREAL_1:1;

A31: f2 is onto by A15, FUNCT_2:def 3;

then A32: (f2 ") . p1 = (f4 ") . p1 by A14, TOPS_2:def 4;

A33: (f2 ") . p2 = (f4 ") . p2 by A14, A31, TOPS_2:def 4;

A34: g . 0 = 0 by A12, A14, A26, A29, A32, FUNCT_1:32;

A35: g . 1 = 1 by A13, A14, A27, A30, A33, FUNCT_1:32;

the Element of P2 \ P1 in the carrier of ((TOP-REAL n) | P29) by A5, PRE_TOPC:8;

then A36: (f2 ") . the Element of P2 \ P1 in the carrier of I[01] by FUNCT_2:5;

A44: rng f2 = [#] ((TOP-REAL n) | P2) by A11, TOPS_2:def 5

.= P2 by PRE_TOPC:def 5 ;

A45: r <= 1 by A36, BORSUK_1:40, XXREAL_1:1;

r < 1 by A45, A48, XXREAL_0:1;

then consider rc being Real such that

A51: g . rc = r and

A52: 0 < rc and

A53: rc < 1 by A34, A35, A50, TOPREAL5:6;

the carrier of ((TOP-REAL n) | P1) = [#] ((TOP-REAL n) | P1)

.= P1 by PRE_TOPC:def 5 ;

then rng f1 c= dom (f2 ") by A3, A17;

then dom g = dom f1 by A18, RELAT_1:27

.= [#] I[01] by A7, TOPS_2:def 5

.= [.0,1.] by BORSUK_1:40 ;

then rc in dom g by A52, A53, XXREAL_1:1;

hence contradiction by A37, A51, FUNCT_1:def 3; :: thesis: verum

end;set p = the Element of P2 \ P1;

A5: the Element of P2 \ P1 in P2 by A4, XBOOLE_0:def 5;

A6: not the Element of P2 \ P1 in P1 by A4, XBOOLE_0:def 5;

consider f1 being Function of I[01],((TOP-REAL n) | P19) such that

A7: f1 is being_homeomorphism and

A8: f1 . 0 = p1 and

A9: f1 . 1 = p2 by A1, TOPREAL1:def 1;

A10: f1 is continuous by A7, TOPS_2:def 5;

consider f2 being Function of I[01],((TOP-REAL n) | P29) such that

A11: f2 is being_homeomorphism and

A12: f2 . 0 = p1 and

A13: f2 . 1 = p2 by A2, TOPREAL1:def 1;

reconsider f4 = f2 as Function ;

A14: f2 is one-to-one by A11, TOPS_2:def 5;

A15: rng f2 = [#] ((TOP-REAL n) | P2) by A11, TOPS_2:def 5;

A16: f2 " is being_homeomorphism by A11, TOPS_2:56;

then A17: dom (f2 ") = [#] ((TOP-REAL n) | P2) by TOPS_2:def 5

.= P2 by PRE_TOPC:def 5 ;

f2 " is continuous by A11, TOPS_2:def 5;

then consider h being Function of I[01],I[01] such that

A18: h = (f2 ") * f1 and

A19: h is continuous by A3, A10, Th45;

reconsider h1 = h as Function of (Closed-Interval-TSpace (0,1)),R^1 by BORSUK_1:40, FUNCT_2:7, TOPMETR:17, TOPMETR:20;

for F1 being Subset of R^1 st F1 is closed holds

h1 " F1 is closed

proof

then reconsider g = h1 as continuous Function of (Closed-Interval-TSpace (0,1)),R^1 by PRE_TOPC:def 6;
let F1 be Subset of R^1; :: thesis: ( F1 is closed implies h1 " F1 is closed )

assume A20: F1 is closed ; :: thesis: h1 " F1 is closed

reconsider K = the carrier of I[01] as Subset of R^1 by BORSUK_1:40, TOPMETR:17;

A21: I[01] = R^1 | K by BORSUK_1:40, TOPMETR:19, TOPMETR:20;

reconsider P3 = F1 /\ K as Subset of (R^1 | K) by TOPS_2:29;

A22: P3 is closed by A20, Th2;

h1 " K = the carrier of I[01] by FUNCT_2:40

.= dom h1 by FUNCT_2:def 1 ;

then h1 " F1 = (h1 " F1) /\ (h1 " K) by RELAT_1:132, XBOOLE_1:28

.= h " P3 by FUNCT_1:68 ;

hence h1 " F1 is closed by A19, A21, A22, TOPMETR:20; :: thesis: verum

end;assume A20: F1 is closed ; :: thesis: h1 " F1 is closed

reconsider K = the carrier of I[01] as Subset of R^1 by BORSUK_1:40, TOPMETR:17;

A21: I[01] = R^1 | K by BORSUK_1:40, TOPMETR:19, TOPMETR:20;

reconsider P3 = F1 /\ K as Subset of (R^1 | K) by TOPS_2:29;

A22: P3 is closed by A20, Th2;

h1 " K = the carrier of I[01] by FUNCT_2:40

.= dom h1 by FUNCT_2:def 1 ;

then h1 " F1 = (h1 " F1) /\ (h1 " K) by RELAT_1:132, XBOOLE_1:28

.= h " P3 by FUNCT_1:68 ;

hence h1 " F1 is closed by A19, A21, A22, TOPMETR:20; :: thesis: verum

A23: dom f1 = [#] I[01] by A7, TOPS_2:def 5

.= [.0,1.] by BORSUK_1:40 ;

then A24: 0 in dom f1 by XXREAL_1:1;

A25: 1 in dom f1 by A23, XXREAL_1:1;

A26: g . 0 = (f2 ") . p1 by A8, A18, A24, FUNCT_1:13;

A27: g . 1 = (f2 ") . p2 by A9, A18, A25, FUNCT_1:13;

A28: dom f2 = [#] I[01] by A11, TOPS_2:def 5

.= [.0,1.] by BORSUK_1:40 ;

then A29: 0 in dom f2 by XXREAL_1:1;

A30: 1 in dom f2 by A28, XXREAL_1:1;

A31: f2 is onto by A15, FUNCT_2:def 3;

then A32: (f2 ") . p1 = (f4 ") . p1 by A14, TOPS_2:def 4;

A33: (f2 ") . p2 = (f4 ") . p2 by A14, A31, TOPS_2:def 4;

A34: g . 0 = 0 by A12, A14, A26, A29, A32, FUNCT_1:32;

A35: g . 1 = 1 by A13, A14, A27, A30, A33, FUNCT_1:32;

the Element of P2 \ P1 in the carrier of ((TOP-REAL n) | P29) by A5, PRE_TOPC:8;

then A36: (f2 ") . the Element of P2 \ P1 in the carrier of I[01] by FUNCT_2:5;

A37: now :: thesis: not (f2 ") . the Element of P2 \ P1 in rng g

reconsider r = (f2 ") . the Element of P2 \ P1 as Real ;assume
(f2 ") . the Element of P2 \ P1 in rng g
; :: thesis: contradiction

then consider x being object such that

A38: x in dom g and

A39: (f2 ") . the Element of P2 \ P1 = g . x by FUNCT_1:def 3;

A40: (f2 ") . the Element of P2 \ P1 = (f2 ") . (f1 . x) by A18, A38, A39, FUNCT_1:12;

A41: x in dom f1 by A18, A38, FUNCT_1:11;

A42: f1 . x in dom (f2 ") by A18, A38, FUNCT_1:11;

f2 " is one-to-one by A16, TOPS_2:def 5;

then the Element of P2 \ P1 = f1 . x by A5, A17, A40, A42, FUNCT_1:def 4;

then A43: the Element of P2 \ P1 in rng f1 by A41, FUNCT_1:def 3;

rng f1 = [#] ((TOP-REAL n) | P1) by A7, TOPS_2:def 5

.= P1 by PRE_TOPC:def 5 ;

hence contradiction by A4, A43, XBOOLE_0:def 5; :: thesis: verum

end;then consider x being object such that

A38: x in dom g and

A39: (f2 ") . the Element of P2 \ P1 = g . x by FUNCT_1:def 3;

A40: (f2 ") . the Element of P2 \ P1 = (f2 ") . (f1 . x) by A18, A38, A39, FUNCT_1:12;

A41: x in dom f1 by A18, A38, FUNCT_1:11;

A42: f1 . x in dom (f2 ") by A18, A38, FUNCT_1:11;

f2 " is one-to-one by A16, TOPS_2:def 5;

then the Element of P2 \ P1 = f1 . x by A5, A17, A40, A42, FUNCT_1:def 4;

then A43: the Element of P2 \ P1 in rng f1 by A41, FUNCT_1:def 3;

rng f1 = [#] ((TOP-REAL n) | P1) by A7, TOPS_2:def 5

.= P1 by PRE_TOPC:def 5 ;

hence contradiction by A4, A43, XBOOLE_0:def 5; :: thesis: verum

A44: rng f2 = [#] ((TOP-REAL n) | P2) by A11, TOPS_2:def 5

.= P2 by PRE_TOPC:def 5 ;

A45: r <= 1 by A36, BORSUK_1:40, XXREAL_1:1;

A46: now :: thesis: not r = 0

assume A47:
r = 0
; :: thesis: contradiction

f2 . r = f4 . ((f4 ") . the Element of P2 \ P1) by A31, A14, TOPS_2:def 4

.= the Element of P2 \ P1 by A5, A14, A44, FUNCT_1:35 ;

hence contradiction by A1, A6, A12, A47, TOPREAL1:1; :: thesis: verum

end;f2 . r = f4 . ((f4 ") . the Element of P2 \ P1) by A31, A14, TOPS_2:def 4

.= the Element of P2 \ P1 by A5, A14, A44, FUNCT_1:35 ;

hence contradiction by A1, A6, A12, A47, TOPREAL1:1; :: thesis: verum

A48: now :: thesis: not r = 1

A50:
0 < r
by A36, A46, BORSUK_1:40, XXREAL_1:1;assume A49:
r = 1
; :: thesis: contradiction

f2 . r = f4 . ((f4 ") . the Element of P2 \ P1) by A31, A14, TOPS_2:def 4

.= the Element of P2 \ P1 by A5, A14, A44, FUNCT_1:35 ;

hence contradiction by A1, A6, A13, A49, TOPREAL1:1; :: thesis: verum

end;f2 . r = f4 . ((f4 ") . the Element of P2 \ P1) by A31, A14, TOPS_2:def 4

.= the Element of P2 \ P1 by A5, A14, A44, FUNCT_1:35 ;

hence contradiction by A1, A6, A13, A49, TOPREAL1:1; :: thesis: verum

r < 1 by A45, A48, XXREAL_0:1;

then consider rc being Real such that

A51: g . rc = r and

A52: 0 < rc and

A53: rc < 1 by A34, A35, A50, TOPREAL5:6;

the carrier of ((TOP-REAL n) | P1) = [#] ((TOP-REAL n) | P1)

.= P1 by PRE_TOPC:def 5 ;

then rng f1 c= dom (f2 ") by A3, A17;

then dom g = dom f1 by A18, RELAT_1:27

.= [#] I[01] by A7, TOPS_2:def 5

.= [.0,1.] by BORSUK_1:40 ;

then rc in dom g by A52, A53, XXREAL_1:1;

hence contradiction by A37, A51, FUNCT_1:def 3; :: thesis: verum

hence P1 = P2 by A3; :: thesis: verum