Copyright (c) 1997 Association of Mizar Users
environ
vocabulary ARYTM_1, EUCLID, PRE_TOPC, BORSUK_1, RELAT_1, TOPREAL1, FUNCT_1,
TOPS_2, SUBSET_1, ORDINAL2, BOOLE, COMPTS_1, JORDAN3, RCOMP_1, FINSEQ_1,
TREAL_1, SEQ_1, TOPMETR, JORDAN5C, FINSEQ_4;
notation TARSKI, XBOOLE_0, SUBSET_1, XREAL_0, REAL_1, NAT_1, RCOMP_1, RELAT_1,
FINSEQ_1, FUNCT_1, FUNCT_2, TOPMETR, FINSEQ_4, JORDAN3, STRUCT_0,
TOPREAL1, PRE_TOPC, TOPS_2, COMPTS_1, EUCLID, TREAL_1;
constructors REAL_1, NAT_1, TOPS_2, COMPTS_1, RCOMP_1, TREAL_1, JORDAN3,
TOPREAL1, FINSEQ_4, MEMBERED;
clusters BORSUK_1, EUCLID, FUNCT_1, PRE_TOPC, RELSET_1, STRUCT_0, XREAL_0,
ARYTM_3, MEMBERED;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
definitions TARSKI, JORDAN3, XBOOLE_0;
theorems AXIOMS, BORSUK_1, COMPTS_1, EUCLID, FUNCT_1, FUNCT_2, RELAT_1,
JORDAN3, GOBOARD1, NAT_1, GOBOARD9, SPPOL_1, TOPS_1, GOBOARD2, PRE_TOPC,
RCOMP_1, REAL_1, HEINE, PCOMPS_1, SPPOL_2, TARSKI, TOPMETR, TOPREAL1,
TOPREAL3, RFUNCT_2, TSEP_1, JORDAN5B, TOPS_2, TREAL_1, JORDAN5A,
ZFMISC_1, PARTFUN2, RELSET_1, XBOOLE_0, XBOOLE_1, FINSEQ_3, XCMPLX_1;
schemes NAT_1;
begin :: First and last point of a curve
Lm1:
for r be Real st 0 <= r & r <= 1 holds 0 <= 1-r & 1-r <= 1
proof
let r be Real; assume 0 <= r & r <= 1;
then 1-1 <= 1-r & 1-r <= 1-0 by REAL_1:92;
hence thesis;
end;
theorem Th1: :: Characterization of First Point Intersecting Q
for P, Q being Subset of TOP-REAL 2,
p1, p2, q1 being Point of TOP-REAL 2,
f being map of I[01], (TOP-REAL 2)|P, s1 be Real
st P is_an_arc_of p1,p2 & q1 in P & q1 in Q & f.s1 = q1 & f is_homeomorphism
& f.0 = p1 & f.1 = p2 & 0 <= s1 & s1 <= 1 &
(for t being Real st 0 <= t & t < s1 holds not f.t in Q) holds
for g being map of I[01], (TOP-REAL 2)|P, s2 be Real st
g is_homeomorphism & g.0 = p1 & g.1 = p2 & g.s2 = q1
& 0 <= s2 & s2 <= 1 holds
(for t being Real st 0 <= t & t < s2 holds not g.t in Q)
proof
let P, Q be Subset of TOP-REAL 2,
p1, p2, q1 be Point of TOP-REAL 2,
f be map of I[01], (TOP-REAL 2)|P, s1 be Real;
assume
A1: P is_an_arc_of p1,p2 & q1 in P & q1 in Q & f.s1=q1 & f is_homeomorphism
& f.0=p1 & f.1=p2 & 0 <= s1 & s1 <= 1 &
(for t being Real st 0<=t & t<s1 holds not f.t in Q);
then reconsider P'=P as non empty Subset of TOP-REAL 2;
let g be map of I[01], (TOP-REAL 2)|P, s2 be Real;
assume A2: g is_homeomorphism & g.0=p1 & g.1=p2 & g.s2=q1
& 0<=s2 & s2<=1;
let t be Real; assume A3: 0<=t & t<s2;
then A4: t <= 1 by A2,AXIOMS:22;
reconsider f,g as map of I[01], (TOP-REAL 2)|P';
set fg = f"*g;
A5: f" is_homeomorphism by A1,TOPS_2:70;
then A6: fg is_homeomorphism by A2,TOPS_2:71;
A7: dom f = [#]I[01] & rng f = [#]((TOP-REAL 2)|P) by A1,TOPS_2:def 5;
then A8: dom f = the carrier of I[01] & rng f = the carrier of ((TOP-REAL 2)|P)
by PRE_TOPC:12;
then A9: 0 in dom f & 1 in dom f by JORDAN5A:2;
A10: f is one-to-one by A1,TOPS_2:def 5;
A11: fg is continuous & fg is one-to-one by A6,TOPS_2:def 5;
A12: f".p1 = (f qua Function)".p1 by A7,A10,TOPS_2:def 4
.= 0 by A1,A9,A10,FUNCT_1:54;
A13: dom (f") = [#]((TOP-REAL 2)|P) by A5,TOPS_2:def 5;
A14: f".p2 = (f qua Function)".p2 by A7,A10,TOPS_2:def 4
.= 1 by A1,A9,A10,FUNCT_1:54;
A15: dom g = [#]I[01] & rng g = [#]((TOP-REAL 2)|P) by A2,TOPS_2:def 5;
then A16: dom g = the carrier of I[01] by PRE_TOPC:12;
then 0 in dom g by JORDAN5A:2;
then A17: (f"*g).0 = 0 by A2,A12,FUNCT_1:23;
1 in dom g by A16,JORDAN5A:2;
then A18: (f"*g).1 = 1 by A2,A14,FUNCT_1:23;
A19: s1 in dom f by A1,A8,JORDAN5A:2;
s2 in dom g by A2,A16,JORDAN5A:2;
then A20: (f"*g).s2 = f".q1 by A2,FUNCT_1:23
.= (f qua Function)".q1 by A7,A10,TOPS_2:def 4
.= s1 by A1,A10,A19,FUNCT_1:54;
reconsider t1 = t, s2' = s2 as Point of I[01]
by A2,A3,A4,JORDAN5A:2;
A21: t in the carrier of I[01] by A3,A4,JORDAN5A:2;
then fg.t in the carrier of I[01] by FUNCT_2:7;
then reconsider Ft = fg.t1 as Real by BORSUK_1:83;
A22: 0 <= Ft
proof
per cases by A3;
suppose 0<t;
hence thesis by A11,A17,A18,BORSUK_1:def 17,JORDAN5A:16,TOPMETR:27;
suppose 0 = t;
hence thesis by A2,A12,A16,FUNCT_1:23;
end;
fg.s2' = s1 by A20;
then A23: Ft < s1 by A3,A11,A17,A18,JORDAN5A:16,TOPMETR:27;
A24: f*(f"*g) = (g qua Relation) * (f * f") by RELAT_1:55
.= (g qua Relation) * id rng f by A7,A10,TOPS_2:65
.= id rng g * g by A2,A7,TOPS_2:def 5
.= g by FUNCT_1:42;
dom (f"*g) = dom g by A13,A15,RELAT_1:46;
then f.((f"*g).t) = g.t by A16,A21,A24,FUNCT_1:23;
hence thesis by A1,A22,A23;
end;
definition
let P, Q be Subset of TOP-REAL 2,
p1, p2 be Point of TOP-REAL 2;
assume A1: P meets Q & P /\ Q is closed & P is_an_arc_of p1,p2;
func First_Point(P,p1,p2,Q) -> Point of TOP-REAL 2 means
:Def1: it in P /\ Q &
for g being map of I[01], (TOP-REAL 2)|P, s2 being Real st
g is_homeomorphism & g.0 = p1 & g.1 = p2
& g.s2 = it & 0 <= s2 & s2 <= 1 holds
(for t being Real st 0 <= t & t < s2 holds not g.t in Q);
existence
proof
consider EX be Point of TOP-REAL 2 such that
A2: EX in P /\ Q &
ex g being map of I[01], (TOP-REAL 2)|P, s2 be Real st
g is_homeomorphism & g.0=p1 & g.1=p2 &
g.s2=EX & 0<=s2 & s2<=1 &
(for t being Real st 0<=t & t<s2 holds not g.t in Q)
by A1,JORDAN5A:22;
EX in P & EX in Q by A2,XBOOLE_0:def 3;
then for g being map of I[01], (TOP-REAL 2)|P, s2 be Real st
g is_homeomorphism & g.0=p1 & g.1=p2
& g.s2=EX & 0<=s2 & s2<=1 holds
(for t being Real st 0<=t & t<s2 holds not g.t in Q) by A1,A2,Th1;
hence thesis by A2;
end;
uniqueness
proof
let IT1, IT2 be Point of TOP-REAL 2;
A3: P /\ Q c= Q & P /\ Q c= P by XBOOLE_1:17;
assume
A4: IT1 in P /\ Q &
for g1 being map of I[01], (TOP-REAL 2)|P, s1 be Real st
g1 is_homeomorphism & g1.0=p1 & g1.1=p2
& g1.s1=IT1 & 0<=s1 & s1<=1 holds
(for t being Real st 0<=t & t<s1 holds not g1.t in Q);
assume
A5: IT2 in P /\ Q &
for g2 being map of I[01], (TOP-REAL 2)|P, s2 be Real st
g2 is_homeomorphism & g2.0=p1 & g2.1=p2
& g2.s2=IT2 & 0<=s2 & s2<=1 holds
(for t being Real st 0<=t & t<s2 holds not g2.t in Q);
consider g be map of I[01], (TOP-REAL 2)|P such that
A6: g is_homeomorphism & g.0=p1 & g.1=p2 by A1,TOPREAL1:def 2;
A7: rng g = [#]((TOP-REAL 2)|P) by A6,TOPS_2:def 5
.= P by PRE_TOPC:def 10;
A8: dom g = [#]I[01] by A6,TOPS_2:def 5
.= the carrier of I[01] by PRE_TOPC:12;
consider ss1 be set such that
A9: ss1 in dom g & g.ss1 = IT1 by A3,A4,A7,FUNCT_1:def 5;
reconsider ss1 as Real by A8,A9,BORSUK_1:83;
consider ss2 be set such that
A10: ss2 in dom g & g.ss2 = IT2 by A3,A5,A7,FUNCT_1:def 5;
reconsider ss2 as Real by A8,A10,BORSUK_1:83;
A11:0 <= ss1 & ss1 <= 1 & 0 <= ss2 & ss2 <= 1 by A8,A9,A10,JORDAN5A:2;
per cases by REAL_1:def 5;
suppose ss1 < ss2;
hence thesis by A3,A4,A5,A6,A9,A10,A11;
suppose ss1 = ss2;
hence thesis by A9,A10;
suppose ss1 > ss2;
hence thesis by A3,A4,A5,A6,A9,A10,A11;
end;
end;
theorem
for P, Q being Subset of TOP-REAL 2,
p, p1, p2 being Point of TOP-REAL 2 st
p in P & P is_an_arc_of p1, p2 & Q = {p} holds
First_Point (P,p1,p2,Q) = p
proof
let P, Q be Subset of TOP-REAL 2,
p, p1, p2 be Point of TOP-REAL 2;
A1: TOP-REAL 2 is_T2 by SPPOL_1:26;
assume A2: p in P & P is_an_arc_of p1, p2 & Q = {p};
then A3: P /\ {p} = {p} by ZFMISC_1:52;
then A4: p in P /\ {p} by TARSKI:def 1;
then A5: P meets {p} & P /\ Q is closed & P is_an_arc_of p1,p2
by A1,A2,A3,PCOMPS_1:10,XBOOLE_0:3;
for g being map of I[01], (TOP-REAL 2)|P, s2 be Real st
g is_homeomorphism & g.0=p1 & g.1=p2
& g.s2=p & 0<=s2 & s2<=1 holds
(for t being Real st 0<=t & t<s2 holds not g.t in {p})
proof
let g be map of I[01], (TOP-REAL 2)|P, s2 be Real; assume
A6: g is_homeomorphism & g.0=p1 & g.1=p2
& g.s2=p & 0<=s2 & s2<=1;
then A7: g is one-to-one by TOPS_2:def 5;
[#]((TOP-REAL 2)|P) <> {} by A2,PRE_TOPC:def 10;
then the carrier of I[01] <> {} & the carrier of ((TOP-REAL 2)|P) <> {}
by PRE_TOPC:12;
then A8: dom g = the carrier of I[01] by FUNCT_2:def 1;
let t be Real; assume A9: 0<=t & t<s2;
then t <= 1 by A6,AXIOMS:22;
then s2 in dom g & t in dom g & s2 <> t by A6,A8,A9,JORDAN5A:2;
then g.t <> g.s2 by A7,FUNCT_1:def 8;
hence thesis by A6,TARSKI:def 1;
end;
hence thesis by A2,A4,A5,Def1;
end;
theorem Th3:
for P being Subset of TOP-REAL 2,
Q being Subset of TOP-REAL 2,
p1, p2 being Point of TOP-REAL 2 st
p1 in Q & P /\ Q is closed & P is_an_arc_of p1, p2 holds
First_Point (P, p1, p2, Q) = p1
proof
let P be Subset of TOP-REAL 2,
Q be Subset of TOP-REAL 2,
p1,p2 be Point of TOP-REAL 2;
assume A1: p1 in Q & P /\ Q is closed & P is_an_arc_of p1, p2;
then A2:p1 in P by TOPREAL1:4;
then A3: p1 in P /\ Q by A1,XBOOLE_0:def 3;
A4: P meets Q by A1,A2,XBOOLE_0:3;
for g being map of I[01], (TOP-REAL 2)|P, s2 be Real st
g is_homeomorphism & g.0=p1 & g.1=p2
& g.s2=p1 & 0<=s2 & s2<=1 holds
(for t being Real st 0<=t & t<s2 holds not g.t in Q)
proof
let g be map of I[01], (TOP-REAL 2)|P, s2 be Real;
assume A5: g is_homeomorphism & g.0=p1 & g.1=p2
& g.s2=p1 & 0<=s2 & s2<=1;
then dom g = [#] I[01] by TOPS_2:def 5
.= the carrier of I[01] by PRE_TOPC:12;
then A6: s2 in dom g & 0 in dom g by A5,JORDAN5A:2;
A7: g is one-to-one by A5,TOPS_2:def 5;
let t be Real; assume 0<=t & t<s2;
hence thesis by A5,A6,A7,FUNCT_1:def 8;
end;
hence thesis by A1,A3,A4,Def1;
end;
theorem ::Characterization of Last Point Intersecting Q
Th4:
for P, Q being Subset of TOP-REAL 2,
p1, p2, q1 being Point of TOP-REAL 2,
f being map of I[01], (TOP-REAL 2)|P,
s1 be Real
st P is_an_arc_of p1,p2 & q1 in P & q1 in Q & f.s1 = q1 &
f is_homeomorphism & f.0 = p1 & f.1 = p2 & 0 <= s1 & s1 <= 1 &
(for t being Real st 1 >= t & t > s1 holds not f.t in Q) holds
for g being map of I[01], (TOP-REAL 2)|P, s2 being Real st
g is_homeomorphism
& g.0 = p1 & g.1 = p2 & g.s2 = q1
& 0 <= s2 & s2 <= 1 holds
(for t being Real st 1 >= t & t > s2 holds not g.t in Q)
proof
let P, Q be Subset of TOP-REAL 2,
p1, p2, q1 be Point of TOP-REAL 2,
f be map of I[01], (TOP-REAL 2)|P, s1 be Real;
assume
A1: P is_an_arc_of p1,p2 & q1 in P & q1 in Q & f.s1=q1 & f is_homeomorphism
& f.0=p1 & f.1=p2 & 0 <= s1 & s1 <= 1 &
(for t being Real st 1>=t & t>s1 holds not f.t in Q);
let g be map of I[01], (TOP-REAL 2)|P, s2 be Real;
reconsider P'=P as non empty Subset of TOP-REAL 2 by A1;
assume A2: g is_homeomorphism & g.0=p1 & g.1=p2 & g.s2=q1
& 0<=s2 & s2<=1;
reconsider f, g as map of I[01], (TOP-REAL 2)|P';
let t be Real; assume A3: 1>=t & t>s2;
then A4: 0 <= t by A2,AXIOMS:22;
set fg = f"*g;
A5: f" is_homeomorphism by A1,TOPS_2:70;
then A6: fg is_homeomorphism by A2,TOPS_2:71;
A7: dom f = [#]I[01] & rng f = [#]((TOP-REAL 2)|P) by A1,TOPS_2:def 5;
then A8: dom f = the carrier of I[01] & rng f = the carrier of ((TOP-REAL 2)|P)
by PRE_TOPC:12;
then A9: 0 in dom f & 1 in dom f by JORDAN5A:2;
A10: f is one-to-one by A1,TOPS_2:def 5;
A11: fg is continuous & fg is one-to-one by A6,TOPS_2:def 5;
A12: f".p1 = (f qua Function)".p1 by A7,A10,TOPS_2:def 4
.= 0 by A1,A9,A10,FUNCT_1:54;
A13: dom (f") = [#]((TOP-REAL 2)|P) by A5,TOPS_2:def 5;
A14: f".p2 = (f qua Function)".p2 by A7,A10,TOPS_2:def 4
.= 1 by A1,A9,A10,FUNCT_1:54;
A15: dom g = [#]I[01] & rng g = [#]((TOP-REAL 2)|P) by A2,TOPS_2:def 5;
then A16: dom g = the carrier of I[01] by PRE_TOPC:12;
then 0 in dom g by JORDAN5A:2;
then A17: (f"*g).0 = 0 by A2,A12,FUNCT_1:23;
1 in dom g by A16,JORDAN5A:2;
then A18: (f"*g).1 = 1 by A2,A14,FUNCT_1:23;
A19: s1 in dom f by A1,A8,JORDAN5A:2;
s2 in dom g by A2,A16,JORDAN5A:2;
then A20: (f"*g).s2 = f".q1 by A2,FUNCT_1:23
.= (f qua Function)".q1 by A7,A10,TOPS_2:def 4
.= s1 by A1,A10,A19,FUNCT_1:54;
reconsider t1 = t, s2' = s2 as Point of I[01]
by A2,A3,A4,JORDAN5A:2;
A21: t in the carrier of I[01] by A3,A4,JORDAN5A:2;
then fg.t in the carrier of I[01] by FUNCT_2:7;
then reconsider Ft = fg.t1 as Real by BORSUK_1:83;
A22: Ft <= 1
proof
per cases by A3,REAL_1:def 5;
suppose t<1;
hence thesis by A11,A17,A18,BORSUK_1:def 18,JORDAN5A:16,TOPMETR:27
;
suppose t=1;
hence thesis by A2,A14,A16,FUNCT_1:23;
end;
fg.s2' = s1 by A20;
then A23: s1 < Ft by A3,A11,A17,A18,JORDAN5A:16,TOPMETR:27;
A24: f*(f"*g) = (g qua Relation) * (f * f") by RELAT_1:55
.= (g qua Relation) * id rng f by A7,A10,TOPS_2:65
.= id rng g * g by A2,A7,TOPS_2:def 5
.= g by FUNCT_1:42;
t in dom (f"*g) by A13,A15,A16,A21,RELAT_1:46;
then f.((f"*g).t) = g.t by A24,FUNCT_1:23;
hence thesis by A1,A22,A23;
end;
definition
let P, Q be Subset of TOP-REAL 2,
p1,p2 be Point of TOP-REAL 2;
assume A1: P meets Q & P /\ Q is closed & P is_an_arc_of p1,p2;
func Last_Point (P,p1,p2,Q) -> Point of TOP-REAL 2 means
:Def2: it in P /\ Q &
for g being map of I[01], (TOP-REAL 2)|P, s2 be Real st
g is_homeomorphism
& g.0 = p1 & g.1 = p2
& g.s2 = it & 0 <= s2 & s2 <= 1 holds
for t being Real st 1 >= t & t > s2 holds not g.t in Q;
existence
proof
consider EX be Point of TOP-REAL 2 such that
A2: EX in P /\ Q &
ex g being map of I[01], (TOP-REAL 2)|P, s2 be Real st
g is_homeomorphism & g.0=p1 & g.1=p2 &
g.s2=EX & 0<=s2 & s2<=1 &
(for t being Real st 1>=t & t>s2 holds not g.t in Q)
by A1,JORDAN5A:23;
EX in P & EX in Q by A2,XBOOLE_0:def 3;
then for g being map of I[01], (TOP-REAL 2)|P, s2 be Real st
g is_homeomorphism & g.0=p1 & g.1=p2
& g.s2=EX & 0<=s2 & s2<=1 holds
(for t being Real st 1>=t & t>s2 holds not g.t in Q)
by A1,A2,Th4;
hence thesis by A2;
end;
uniqueness
proof
let IT1, IT2 be Point of TOP-REAL 2;
A3: P /\ Q c= Q & P /\ Q c= P by XBOOLE_1:17;
assume
A4: IT1 in P /\ Q &
for g1 being map of I[01], (TOP-REAL 2)|P, s1 be Real st
g1 is_homeomorphism & g1.0=p1 & g1.1=p2
& g1.s1=IT1 & 0<=s1 & s1<=1 holds
(for t being Real st 1>=t & t>s1 holds not g1.t in Q);
assume
A5: IT2 in P /\ Q &
for g2 being map of I[01], (TOP-REAL 2)|P, s2 be Real st
g2 is_homeomorphism & g2.0=p1 & g2.1=p2
& g2.s2=IT2 & 0<=s2 & s2<=1 holds
(for t being Real st 1>=t & t>s2 holds not g2.t in Q);
consider g be map of I[01], (TOP-REAL 2)|P such that
A6: g is_homeomorphism & g.0=p1 & g.1=p2 by A1,TOPREAL1:def 2;
A7: rng g = [#]((TOP-REAL 2)|P) by A6,TOPS_2:def 5
.= P by PRE_TOPC:def 10;
A8: dom g = [#]I[01] by A6,TOPS_2:def 5
.= the carrier of I[01] by PRE_TOPC:12;
consider ss1 be set such that
A9: ss1 in dom g & g.ss1 = IT1 by A3,A4,A7,FUNCT_1:def 5;
reconsider ss1 as Real by A8,A9,BORSUK_1:83;
consider ss2 be set such that
A10: ss2 in dom g & g.ss2 = IT2 by A3,A5,A7,FUNCT_1:def 5;
reconsider ss2 as Real by A8,A10,BORSUK_1:83;
A11:0 <= ss1 & ss1 <= 1 & 0 <= ss2 & ss2 <= 1 by A8,A9,A10,JORDAN5A:2;
per cases by REAL_1:def 5;
suppose ss1 < ss2;
hence thesis by A3,A4,A5,A6,A9,A10,A11;
suppose ss1 = ss2;
hence thesis by A9,A10;
suppose ss1 > ss2;
hence thesis by A3,A4,A5,A6,A9,A10,A11;
end;
end;
theorem
for P, Q being Subset of TOP-REAL 2,
p, p1,p2 being Point of TOP-REAL 2 st
p in P & P is_an_arc_of p1, p2 & Q = {p} holds
Last_Point (P, p1, p2, Q) = p
proof
let P, Q be Subset of TOP-REAL 2,
p, p1, p2 be Point of TOP-REAL 2;
A1: TOP-REAL 2 is_T2 by SPPOL_1:26;
assume A2: p in P & P is_an_arc_of p1, p2 & Q = {p};
then A3: P /\ {p} = {p} by ZFMISC_1:52;
then A4: p in P /\ {p} by TARSKI:def 1;
then A5: P meets {p} & P /\ Q is closed & P is_an_arc_of p1,p2
by A1,A2,A3,PCOMPS_1:10,XBOOLE_0:3;
for g being map of I[01], (TOP-REAL 2)|P, s2 be Real st
g is_homeomorphism & g.0=p1 & g.1=p2
& g.s2=p & 0<=s2 & s2<=1 holds
(for t being Real st 1>=t & t>s2 holds not g.t in {p})
proof
let g be map of I[01], (TOP-REAL 2)|P, s2 be Real; assume
A6: g is_homeomorphism & g.0=p1 & g.1=p2
& g.s2=p & 0<=s2 & s2<=1;
then A7: g is one-to-one by TOPS_2:def 5;
[#]((TOP-REAL 2)|P) <> {} by A2,PRE_TOPC:def 10;
then the carrier of I[01] <> {} & the carrier of ((TOP-REAL 2)|P) <> {}
by PRE_TOPC:12;
then A8: dom g = the carrier of I[01] by FUNCT_2:def 1;
let t be Real; assume A9: 1>=t & t>s2;
then t >= 0 by A6,AXIOMS:22;
then s2 in dom g & t in dom g & s2 <> t by A6,A8,A9,JORDAN5A:2;
then g.t <> g.s2 by A7,FUNCT_1:def 8;
hence thesis by A6,TARSKI:def 1;
end;
hence thesis by A2,A4,A5,Def2;
end;
theorem Th6:
for P,Q being Subset of TOP-REAL 2,
p1, p2 being Point of TOP-REAL 2 st
p2 in Q & P /\ Q is closed & P is_an_arc_of p1, p2 holds
Last_Point (P, p1, p2, Q) = p2
proof
let P,Q be Subset of TOP-REAL 2,
p1,p2 be Point of TOP-REAL 2;
assume A1: p2 in Q & P /\ Q is closed & P is_an_arc_of p1, p2;
then A2:p2 in P by TOPREAL1:4;
then A3: p2 in P /\ Q by A1,XBOOLE_0:def 3;
A4: P meets Q by A1,A2,XBOOLE_0:3;
for g being map of I[01], (TOP-REAL 2)|P, s2 be Real st
g is_homeomorphism & g.0=p1 & g.1=p2
& g.s2=p2 & 0<=s2 & s2<=1 holds
(for t being Real st 1>=t & t>s2 holds not g.t in Q)
proof
let g be map of I[01], (TOP-REAL 2)|P, s2 be Real;
assume A5: g is_homeomorphism & g.0=p1 & g.1=p2
& g.s2=p2 & 0<=s2 & s2<=1;
then dom g = [#] I[01] by TOPS_2:def 5
.= the carrier of I[01] by PRE_TOPC:12;
then A6: s2 in dom g & 1 in dom g by A5,JORDAN5A:2;
A7: g is one-to-one by A5,TOPS_2:def 5;
let t be Real; assume 1>=t & t>s2;
hence thesis by A5,A6,A7,FUNCT_1:def 8;
end;
hence thesis by A1,A3,A4,Def2;
end;
theorem Th7:
for P being Subset of TOP-REAL 2,
Q being Subset of TOP-REAL 2,
p1, p2 being Point of TOP-REAL 2 st
P c= Q & P is closed & P is_an_arc_of p1, p2 holds
First_Point (P, p1, p2, Q) = p1 &
Last_Point (P, p1, p2, Q) = p2
proof
let P be Subset of TOP-REAL 2,
Q be Subset of TOP-REAL 2,
p1,p2 be Point of TOP-REAL 2;
assume A1: P c= Q & P is closed & P is_an_arc_of p1, p2;
then A2: P /\ Q = P by XBOOLE_1:28;
p1 in P & p2 in P by A1,TOPREAL1:4;
hence thesis by A1,A2,Th3,Th6;
end;
begin :: The ordering of points on a curve
definition let P be Subset of TOP-REAL 2,
p1, p2, q1, q2 be Point of TOP-REAL 2;
pred LE q1, q2, P, p1, p2 means
:Def3: q1 in P & q2 in P &
for g being map of I[01], (TOP-REAL 2)|P,
s1, s2 being Real st
g is_homeomorphism
& g.0 = p1 & g.1 = p2
& g.s1 = q1 & 0 <= s1 & s1 <= 1
& g.s2 = q2 & 0 <= s2 & s2 <= 1
holds s1 <= s2;
end;
theorem Th8:
for P being Subset of TOP-REAL 2,
p1, p2, q1, q2 being Point of TOP-REAL 2,
g being map of I[01], (TOP-REAL 2)|P,
s1, s2 being Real st
P is_an_arc_of p1,p2 & g is_homeomorphism & g.0 = p1 & g.1 = p2
& g.s1 = q1 & 0 <= s1 & s1 <= 1 & g.s2 = q2 & 0 <= s2 & s2 <= 1 & s1 <=
s2 holds
LE q1,q2,P,p1,p2
proof
let P be Subset of TOP-REAL 2,
p1,p2,q1,q2 be Point of TOP-REAL 2,
g be map of I[01], (TOP-REAL 2)|P, s1,s2 be Real;
assume A1: P is_an_arc_of p1,p2 & g is_homeomorphism
& g.0=p1 & g.1=p2
& g.s1=q1 & 0<=s1 & s1<=1
& g.s2=q2 & 0<=s2 & s2<=1 & s1<=s2;
then reconsider P' = P as non empty Subset of TOP-REAL 2 by
TOPREAL1:4;
reconsider g as map of I[01], (TOP-REAL 2)|P';
A2: s1 in the carrier of I[01] by A1,JORDAN5A:2;
then g.s1 in the carrier of ((TOP-REAL 2)|P') by FUNCT_2:7;
then A3: q1 in [#]((TOP-REAL 2)|P') by A1,PRE_TOPC:12;
A4: s2 in the carrier of I[01] by A1,JORDAN5A:2;
then g.s2 in the carrier of ((TOP-REAL 2)|P') by FUNCT_2:7;
then q2 in [#]((TOP-REAL 2)|P') by A1,PRE_TOPC:12;
then A5: q1 in P & q2 in P by A3,PRE_TOPC:def 10;
now let h be map of I[01], (TOP-REAL 2)|P', t1,t2 be Real;
assume A6: h is_homeomorphism & h.0=p1 & h.1=p2
& h.t1=q1 & 0<=t1 & t1<=1 & h.t2=q2 & 0<=t2 & t2<=1;
set hg = h"*g;
h" is_homeomorphism by A6,TOPS_2:70;
then A7: hg is_homeomorphism by A1,TOPS_2:71;
A8: dom h = [#]I[01] & rng h = [#]((TOP-REAL 2)|P) by A6,TOPS_2:def 5;
then A9: dom h = the carrier of I[01] & rng h = the carrier of ((TOP-REAL 2)|P)
by PRE_TOPC:12;
then A10: 0 in dom h & 1 in dom h by JORDAN5A:2;
A11: h is one-to-one by A6,TOPS_2:def 5;
A12: hg is continuous & hg is one-to-one by A7,TOPS_2:def 5;
A13: h".p1 = (h qua Function)".p1 by A8,A11,TOPS_2:def 4
.= 0 by A6,A10,A11,FUNCT_1:54;
A14: h".p2 = (h qua Function)".p2 by A8,A11,TOPS_2:def 4
.= 1 by A6,A10,A11,FUNCT_1:54;
dom g = [#]I[01] & rng g = [#]((TOP-REAL 2)|P) by A1,TOPS_2:def 5;
then A15: dom g = the carrier of I[01] by PRE_TOPC:12;
then 0 in dom g by JORDAN5A:2;
then A16: (h"*g).0 = 0 by A1,A13,FUNCT_1:23;
1 in dom g by A15,JORDAN5A:2;
then A17: (h"*g).1 = 1 by A1,A14,FUNCT_1:23;
A18: t1 in dom h by A6,A9,JORDAN5A:2;
s1 in dom g by A1,A15,JORDAN5A:2;
then A19: (h"*g).s1 = h".q1 by A1,FUNCT_1:23
.= (h qua Function)".q1 by A8,A11,TOPS_2:def 4
.= t1 by A6,A11,A18,FUNCT_1:54;
A20: t2 in dom h by A6,A9,JORDAN5A:2;
s2 in dom g by A1,A15,JORDAN5A:2;
then A21: (h"*g).s2 = h".q2 by A1,FUNCT_1:23
.= (h qua Function)".q2 by A8,A11,TOPS_2:def 4
.= t2 by A6,A11,A20,FUNCT_1:54;
reconsider s1' = s1, s2' = s2 as Point of I[01] by A1,JORDAN5A:2;
hg.s1 in the carrier of I[01] & hg.s2 in the carrier of I[01]
by A2,A4,FUNCT_2:7;
then reconsider hg1 = hg.s1', hg2 = hg.s2' as Real by BORSUK_1:83;
per cases by A1,REAL_1:def 5;
suppose s1 < s2;
then hg1 < hg2 by A12,A16,A17,JORDAN5A:17;
hence t1 <= t2 by A19,A21;
suppose s1 = s2;
hence t1 <= t2 by A19,A21;
end;
hence LE q1,q2,P,p1,p2 by A5,Def3;
end;
theorem Th9:
for P being Subset of TOP-REAL 2,
p1,p2,q1 being Point of TOP-REAL 2
st P is_an_arc_of p1,p2 & q1 in P holds
LE q1,q1,P,p1,p2
proof
let P be Subset of TOP-REAL 2,
p1,p2,q1 be Point of TOP-REAL 2;
assume A1: P is_an_arc_of p1,p2 & q1 in P;
then reconsider P as non empty Subset of TOP-REAL 2;
now let g be map of I[01], (TOP-REAL 2)|P, s1,s2 be Real;
assume A2: g is_homeomorphism &
g.0=p1 & g.1=p2 & g.s1=q1 & 0<=s1 & s1<=1 & g.s2=q1 & 0<=s2 & s2<=1;
then A3: s1 in the carrier of I[01] & s2 in the carrier of I[01] by JORDAN5A:2;
g is one-to-one by A2,TOPS_2:def 5;
hence s1 <= s2 by A2,A3,FUNCT_2:25;
end;
hence thesis by A1,Def3;
end;
theorem Th10:
for P being Subset of TOP-REAL 2,
p1,p2,q1 being Point of TOP-REAL 2
st P is_an_arc_of p1,p2 & q1 in P holds
LE p1,q1,P,p1,p2 & LE q1,p2,P,p1,p2
proof
let P be Subset of TOP-REAL 2,
p1,p2,q1 be Point of TOP-REAL 2;
assume A1: P is_an_arc_of p1,p2 & q1 in P;
then reconsider P as non empty Subset of TOP-REAL 2;
A2:p1 in P & p2 in P by A1,TOPREAL1:4;
A3:now let g be map of I[01], (TOP-REAL 2)|P,s1,s2 be Real;
assume A4: g is_homeomorphism &
g.0=p1 & g.1=p2 & g.s1=p1 & 0<=s1 & s1<=1 & g.s2=q1 & 0<=s2 & s2<=1;
then A5: s1 in the carrier of I[01] & s2 in the carrier of I[01]
& 0 in the carrier of I[01] by JORDAN5A:2;
g is one-to-one by A4,TOPS_2:def 5;
hence s1 <= s2 by A4,A5,FUNCT_2:25;
end;
now let g be map of I[01], (TOP-REAL 2)|P,s1,s2 be Real;
assume A6: g is_homeomorphism &
g.0=p1 & g.1=p2 & g.s1=q1 & 0<=s1 & s1<=1 & g.s2=p2 & 0<=s2 & s2<=1;
then A7: s1 in the carrier of I[01] & s2 in the carrier of I[01]
& 1 in the carrier of I[01] by JORDAN5A:2;
g is one-to-one by A6,TOPS_2:def 5;
hence s1 <= s2 by A6,A7,FUNCT_2:25;
end;
hence thesis by A1,A2,A3,Def3;
end;
theorem
for P being Subset of TOP-REAL 2,
p1,p2 being Point of TOP-REAL 2 st P is_an_arc_of p1,p2 holds
LE p1,p2,P,p1,p2
proof
let P be Subset of TOP-REAL 2,
p1,p2 be Point of TOP-REAL 2;
assume A1: P is_an_arc_of p1,p2;
then p2 in P by TOPREAL1:4;
hence thesis by A1,Th10;
end;
theorem Th12:
for P being Subset of TOP-REAL 2,
p1, p2, q1, q2 being Point of TOP-REAL 2 st P is_an_arc_of p1,p2 &
LE q1,q2,P,p1,p2 & LE q2,q1,P,p1,p2 holds q1=q2
proof
let P be Subset of TOP-REAL 2,
p1,p2,q1,q2 be Point of TOP-REAL 2;
assume A1: P is_an_arc_of p1,p2 & LE q1,q2,P,p1,p2 & LE q2,q1,P,p1,p2;
then consider f being map of I[01], (TOP-REAL 2)|P such that
A2: f is_homeomorphism & f.0 = p1 & f.1 = p2 by TOPREAL1:def 2;
A3: dom f = [#]I[01] by A2,TOPS_2:def 5
.= the carrier of I[01] by PRE_TOPC:12;
A4:rng f = [#]((TOP-REAL 2)|P) by A2,TOPS_2:def 5
.= P by PRE_TOPC:def 10;
then q2 in rng f by A1,Def3;
then consider x be set such that
A5: x in dom f & q2 = f.x by FUNCT_1:def 5;
[.0,1.] = { r1 where r1 is Real : 0 <= r1 & r1 <= 1 } by RCOMP_1:def 1;
then consider s3 being Real such that
A6: s3 = x & 0 <= s3 & s3 <= 1 by A3,A5,BORSUK_1:83;
q1 in rng f by A1,A4,Def3;
then consider y be set such that
A7: y in dom f & q1 = f.y by FUNCT_1:def 5;
[.0,1.] = { r1 where r1 is Real : 0 <= r1 & r1 <= 1 } by RCOMP_1:def 1;
then consider s4 being Real such that
A8: s4 = y & 0 <= s4 & s4 <= 1 by A3,A7,BORSUK_1:83;
A9: s3 <= s4 by A1,A2,A5,A6,A7,A8,Def3;
s4 <= s3 by A1,A2,A5,A6,A7,A8,Def3;
hence q1=q2 by A5,A6,A7,A8,A9,AXIOMS:21;
end;
theorem Th13:
for P being Subset of TOP-REAL 2,
p1,p2,q1,q2,q3 being Point of TOP-REAL 2
st P is_an_arc_of p1,p2 &
LE q1,q2,P,p1,p2 & LE q2,q3,P,p1,p2 holds
LE q1,q3,P,p1,p2
proof
let P be Subset of TOP-REAL 2,
p1,p2,q1,q2,q3 be Point of TOP-REAL 2;
assume A1: P is_an_arc_of p1,p2 & LE q1,q2,P,p1,p2 & LE q2,q3,P,p1,p2;
then A2: q1 in P & q2 in P & for g being map of I[01],
(TOP-REAL 2)|P,s1,s2 being Real
st
g is_homeomorphism & g.0=p1 & g.1=p2
& g.s1=q1 & 0<=s1 & s1<=1
& g.s2=q2 & 0<=s2 & s2<=1 holds s1<=s2 by Def3;
A3: q3 in P & for g being map of I[01], (TOP-REAL 2)|P,s1,s2 being Real st
g is_homeomorphism & g.0=p1 & g.1=p2
& g.s1=q2 & 0<=s1 & s1<=1
& g.s2=q3 & 0<=s2 & s2<=1 holds s1<=s2 by A1,Def3;
now let g be map of I[01], (TOP-REAL 2)|P,s1,s2 be Real;
assume A4: g is_homeomorphism &
g.0=p1 & g.1=p2 & g.s1=q1 & 0<=s1 & s1<=1 & g.s2=q3 & 0<=s2 & s2<=1;
then A5: dom g = [#]I[01] by TOPS_2:def 5
.= the carrier of I[01] by PRE_TOPC:12;
rng g = [#]((TOP-REAL 2)|P) by A4,TOPS_2:def 5
.= P by PRE_TOPC:def 10;
then consider x be set such that
A6: x in dom g & q2 = g.x by A2,FUNCT_1:def 5;
[.0,1.] = { r1 where r1 is Real : 0 <= r1 & r1 <= 1 } by RCOMP_1:def 1;
then consider s3 being Real such that
A7: s3 = x & 0 <= s3 & s3 <= 1 by A5,A6,BORSUK_1:83;
s1 <= s3 & s3 <= s2 by A1,A4,A6,A7,Def3;
hence s1 <= s2 by AXIOMS:22;
end;
hence thesis by A2,A3,Def3;
end;
theorem
for P being Subset of TOP-REAL 2,
p1, p2, q1, q2 being Point of TOP-REAL 2 st
P is_an_arc_of p1, p2 & q1 in P & q2 in P & q1 <> q2
holds
LE q1,q2,P,p1,p2 & not LE q2,q1,P,p1,p2 or
LE q2,q1,P,p1,p2 & not LE q1,q2,P,p1,p2
proof
let P be Subset of TOP-REAL 2,
p1,p2,q1,q2 be Point of TOP-REAL 2;
assume A1: P is_an_arc_of p1,p2 & q1 in P & q2 in P & q1 <> q2;
then reconsider P as non empty Subset of TOP-REAL 2;
not (LE q1,q2,P,p1,p2 iff LE q2,q1,P,p1,p2)
proof
assume A2: LE q1,q2,P,p1,p2 iff LE q2,q1,P,p1,p2;
consider f be map of I[01], (TOP-REAL 2)|P such that
A3: f is_homeomorphism &
f.0 = p1 & f.1 = p2 by A1,TOPREAL1:def 2;
A4: rng f = [#]((TOP-REAL 2)|P) by A3,TOPS_2:def 5
.= P by PRE_TOPC:def 10;
then consider x be set such that A5: x in dom f & q1 = f.x by A1,FUNCT_1:def
5;
consider y be set such that A6: y in dom f & q2 = f.y
by A1,A4,FUNCT_1:def 5;
A7: dom f = [#]I[01] by A3,TOPS_2:def 5
.= [.0,1.] by BORSUK_1:83,PRE_TOPC:12;
then reconsider s1 = x, s2 = y as Real by A5,A6;
A8: f.s1=q1 & 0<=s1 & s1<=1 & f.s2=q2 & 0<=s2 & s2<=1
by A5,A6,A7,BORSUK_1:83,JORDAN5A:2;
per cases by REAL_1:def 5;
suppose s1 < s2;
hence thesis by A1,A2,A3,A8,Th8,Th12;
suppose s1 = s2;
hence thesis by A1,A5,A6;
suppose s1 > s2;
hence thesis by A1,A2,A3,A8,Th8,Th12;
end;
hence thesis;
end;
begin :: Some properties of the ordering of points on a curve
theorem Th15:
for f being FinSequence of TOP-REAL 2,
Q being Subset of TOP-REAL 2,
q being Point of TOP-REAL 2 st
f is_S-Seq & L~f /\ Q is closed & q in L~f & q in Q holds
LE First_Point(L~f,f/.1,f/.len f,Q), q, L~f, f/.1, f/.len f
proof
let f be FinSequence of TOP-REAL 2,
Q be Subset of TOP-REAL 2,
q be Point of TOP-REAL 2;
assume A1: f is_S-Seq & L~f /\ Q is closed & q in L~f & q in Q;
then A2: L~f meets Q by XBOOLE_0:3;
set P = L~f;
A3: P is_an_arc_of f/.1,f/.len f by A1,TOPREAL1:31;
A4: L~f /\ Q c= L~f by XBOOLE_1:17;
set q1 = First_Point(P,f/.1,f/.len f,Q);
A5: q1 in L~f /\ Q by A1,A2,A3,Def1;
for g being map of I[01], (TOP-REAL 2)| P, s1, s2 being Real st
g is_homeomorphism
& g.0=f/.1 & g.1=f/.len f
& g.s1=q1 & 0<=s1 & s1<=1
& g.s2=q & 0<=s2 & s2<=1
holds s1<=s2 by A1,A2,A3,Def1;
hence thesis by A1,A4,A5,Def3;
end;
theorem Th16:
for f being FinSequence of TOP-REAL 2,
Q being Subset of TOP-REAL 2,
q being Point of TOP-REAL 2 st
f is_S-Seq & L~f /\ Q is closed & q in L~f & q in Q holds
LE q, Last_Point(L~f,f/.1,f/.len f,Q), L~f, f/.1, f/.len f
proof
let f be FinSequence of TOP-REAL 2,
Q be Subset of TOP-REAL 2,
q be Point of TOP-REAL 2;
set P = L~f;
assume A1: f is_S-Seq & L~f /\ Q is closed & q in L~f & q in Q;
then A2: L~f meets Q by XBOOLE_0:3;
A3: P is_an_arc_of f/.1,f/.len f by A1,TOPREAL1:31;
A4: L~f /\ Q c= L~f & L~f /\ Q c= Q by XBOOLE_1:17;
set q1 = Last_Point(P,f/.1,f/.len f,Q);
A5: q1 in L~f /\ Q by A1,A2,A3,Def2;
for g being map of I[01], (TOP-REAL 2)| P, s1, s2 being Real st
g is_homeomorphism
& g.0=f/.1 & g.1=f/.len f
& g.s1=q & 0<=s1 & s1<=1
& g.s2=q1 & 0<=s2 & s2<=1
holds s1<=s2 by A1,A2,A3,Def2;
hence thesis by A1,A4,A5,Def3;
end;
theorem Th17:
for q1, q2, p1, p2 being Point of TOP-REAL 2 st p1 <> p2 holds
LE q1, q2, LSeg(p1, p2), p1, p2 implies LE q1, q2, p1, p2
proof
let q1, q2, p1, p2 be Point of TOP-REAL 2;
set P = LSeg (p1, p2);
assume A1: p1 <> p2;
assume A2: LE q1, q2, P, p1, p2;
hence q1 in P & q2 in P by Def3;
let r1,r2 be Real;
assume A3: 0<=r1 & r1<=1 & q1=(1-r1)*p1+r1*p2 &
0<=r2 & r2<=1 & q2=(1-r2)*p1+r2*p2;
consider f be map of I[01], (TOP-REAL 2) | LSeg(p1,p2) such that
A4: (for x being Real st x in [.0,1.] holds f.x = (1-x)*p1 + x*p2) &
f is_homeomorphism & f.0 = p1 & f.1 = p2 by A1,JORDAN5A:4;
r1 in [.0,1.] & r2 in [.0,1.] by A3,BORSUK_1:83,JORDAN5A:2;
then q1 = f.r1 & q2 = f.r2 by A3,A4;
hence thesis by A2,A3,A4,Def3;
end;
theorem
for P, Q being Subset of TOP-REAL 2,
p1, p2 being Point of TOP-REAL 2 st
P is_an_arc_of p1,p2 & P meets Q & P /\ Q is closed holds
First_Point(P,p1,p2,Q) = Last_Point(P,p2,p1,Q) &
Last_Point(P,p1,p2,Q) = First_Point(P,p2,p1,Q)
proof
let P, Q be Subset of TOP-REAL 2,
p1,p2 be Point of TOP-REAL 2;
assume A1: P is_an_arc_of p1,p2 & P /\ Q <> {} & P /\ Q is closed;
then consider x be set such that A2: x in P /\ Q by XBOOLE_0:def 1;
reconsider P as non empty Subset of TOP-REAL 2 by A2;
A3: P is_an_arc_of p2,p1 & P meets Q by A1,JORDAN5B:14,XBOOLE_0:def 7;
then A4: Last_Point(P,p2,p1,Q) in P /\ Q by A1,Def2;
A5: First_Point(P,p2,p1,Q) in P /\ Q & Last_Point(P,p1,p2,Q) in P /\ Q
by A1,A3,Def1,Def2;
A6: for g being map of I[01], (TOP-REAL 2)|P, s2 being Real st
g is_homeomorphism & g.0=p1 & g.1=p2
& g.s2=Last_Point(P,p2,p1,Q) & 0<=s2 & s2<=1 holds
(for t being Real st 0<=t & t<s2 holds not g.t in Q)
proof
let f be map of I[01], (TOP-REAL 2)|P, s2 be Real;
assume A7: f is_homeomorphism & f.0 = p1 & f.1 = p2 &
f.s2 = Last_Point(P,p2,p1,Q) & 0<=s2 & s2<=1;
set Ex = L[01]((0,1)(#),(#)(0,1));
A8: Ex is_homeomorphism by TREAL_1:21;
set g = f * Ex;
A9: Ex.(0,1)(#) = 0 by BORSUK_1:def 17,TREAL_1:8,12;
A10: Ex.(#)(0,1) = 1 by BORSUK_1:def 18,TREAL_1:8,12;
dom f = [#]I[01] by A7,TOPS_2:def 5;
then A11: rng Ex = dom f by A8,TOPMETR:27,TOPS_2:def 5;
then A12: dom g = dom Ex by RELAT_1:46;
rng g = rng f by A11,RELAT_1:47;
then A13: rng g = [#] ((TOP-REAL 2) | P) by A7,TOPS_2:def 5;
dom g = [#]I[01] by A8,A12,TOPMETR:27,TOPS_2:def 5;
then A14: dom g = the carrier of I[01] & rng g = the carrier of ((TOP-REAL 2) |
P)
by A13,PRE_TOPC:12;
then g is Function of the carrier of I[01], the carrier of ((TOP-REAL 2) | P)
by FUNCT_2:def 1,RELSET_1:11;
then reconsider g as map of I[01], (TOP-REAL 2) | P;
A15: g is_homeomorphism by A7,A8,TOPMETR:27,TOPS_2:71;
A16: g.0 = p2 by A7,A10,A14,BORSUK_1:def 17,FUNCT_1:22,TREAL_1:8;
A17: g.1 = p1 by A7,A9,A14,BORSUK_1:def 18,FUNCT_1:22,TREAL_1:8;
let t be Real; assume A18: 0<=t & t<s2;
then A19: t <= 1 by A7,AXIOMS:22;
set s21 = 1 - s2;
A20: 0 <= s21 & s21 <= 1 by A7,Lm1;
A21: 0 <= 1-t & 1-t <= 1 by A18,A19,Lm1;
then reconsider r2 = 1-s2, t' = 1-t as
Point of Closed-Interval-TSpace(0,1)
by A20,JORDAN5A:2,TOPMETR:27;
A22: Ex.r2 = (1-(1-s2))*1 + (1-s2)*0 by BORSUK_1:def 17,def 18,TREAL_1:8,def 3
.= s2 by XCMPLX_1:18;
A23: Ex.t' = (1-(1-t))*1 + (1-t)*0 by BORSUK_1:def 17,def 18,TREAL_1:8,def 3
.= t by XCMPLX_1:18;
s21 in dom g by A14,A20,JORDAN5A:2;
then A24: g.s21 = f.s2 by A22,FUNCT_1:22;
1-t in dom g by A14,A21,JORDAN5A:2;
then A25: g.t' = f.t by A23,FUNCT_1:22;
1-s2 < 1-t by A18,REAL_1:92;
hence thesis by A1,A3,A7,A15,A16,A17,A20,A21,A24,A25,Def2;
end;
for g being map of I[01], (TOP-REAL 2)|P, s2 being Real st
g is_homeomorphism & g.0=p1 & g.1=p2
& g.s2=First_Point(P,p2,p1,Q) & 0<=s2 & s2<=1 holds
(for t being Real st 1>=t & t>s2 holds not g.t in Q)
proof
let f be map of I[01], (TOP-REAL 2)|P, s2 be Real;
assume A26: f is_homeomorphism & f.0 = p1 & f.1 = p2 &
f.s2 = First_Point(P,p2,p1,Q) & 0<=s2 & s2<=1;
set Ex = L[01]((0,1)(#),(#)(0,1));
A27: Ex is_homeomorphism by TREAL_1:21;
set g = f * Ex;
A28: Ex.(0,1)(#) = 0 by BORSUK_1:def 17,TREAL_1:8,12;
A29: Ex.(#)(0,1) = 1 by BORSUK_1:def 18,TREAL_1:8,12;
dom f = [#]I[01] by A26,TOPS_2:def 5;
then A30: rng Ex = dom f by A27,TOPMETR:27,TOPS_2:def 5;
then A31: dom g = dom Ex by RELAT_1:46;
rng g = rng f by A30,RELAT_1:47;
then A32: rng g = [#] ((TOP-REAL 2) | P) by A26,TOPS_2:def 5;
dom g = [#]I[01] by A27,A31,TOPMETR:27,TOPS_2:def 5;
then A33: dom g = the carrier of I[01] & rng g = the carrier of ((TOP-REAL 2) |
P)
by A32,PRE_TOPC:12;
then g is Function of the carrier of I[01], the carrier of ((TOP-REAL 2) | P)
by FUNCT_2:def 1,RELSET_1:11;
then reconsider g as map of I[01], (TOP-REAL 2) | P;
A34: g is_homeomorphism by A26,A27,TOPMETR:27,TOPS_2:71;
A35: g.0 = p2 by A26,A29,A33,BORSUK_1:def 17,FUNCT_1:22,TREAL_1:8;
A36: g.1 = p1 by A26,A28,A33,BORSUK_1:def 18,FUNCT_1:22,TREAL_1:8;
let t be Real; assume A37: 1>=t & t>s2;
then A38: t >= 0 by A26,AXIOMS:22;
set s21 = 1 - s2;
A39: 0 <= s21 & s21 <= 1 by A26,Lm1;
A40: 0 <= 1-t & 1-t <= 1 by A37,A38,Lm1;
then reconsider r2 = 1-s2, t' = 1-t as
Point of Closed-Interval-TSpace(0,1)
by A39,JORDAN5A:2,TOPMETR:27;
A41: Ex.r2 = (1-(1-s2))*1 + (1-s2)*0 by BORSUK_1:def 17,def 18,TREAL_1:8,def 3
.= s2 by XCMPLX_1:18;
A42: Ex.t' = (1-(1-t))*1 + (1-t)*0 by BORSUK_1:def 17,def 18,TREAL_1:8,def 3
.= t by XCMPLX_1:18;
s21 in dom g by A33,A39,JORDAN5A:2;
then A43: g.s21 = f.s2 by A41,FUNCT_1:22;
1-t in dom g by A33,A40,JORDAN5A:2;
then A44: g.t' = f.t by A42,FUNCT_1:22;
1-s2 > 1-t by A37,REAL_1:92;
hence thesis by A1,A3,A26,A34,A35,A36,A39,A40,A43,A44,Def1;
end;
hence thesis by A1,A3,A4,A5,A6,Def1,Def2;
end;
theorem Th19:
for f being FinSequence of TOP-REAL 2,
Q being Subset of TOP-REAL 2,
i being Nat
st L~f meets Q & Q is closed & f is_S-Seq & 1 <= i & i+1 <= len f &
First_Point (L~f, f/.1, f/.len f, Q) in LSeg (f, i) holds
First_Point (L~f, f/.1, f/.len f, Q) =
First_Point (LSeg (f, i), f/.i, f/.(i+1), Q)
proof
let f be FinSequence of TOP-REAL 2,
Q be Subset of TOP-REAL 2,
i be Nat;
A1: L~f is closed by SPPOL_1:49;
assume A2: L~f meets Q & Q is closed & f is_S-Seq & 1 <= i & i+1 <= len f &
First_Point (L~f, f/.1, f/.len f, Q) in LSeg (f, i);
then A3: f is one-to-one by TOPREAL1:def 10;
len f >= 2 by A2,TOPREAL1:def 10;
then reconsider P = L~f, R = LSeg (f, i) as non empty Subset of
the carrier of TOP-REAL 2 by A2,TOPREAL1:29;
A4: L~f meets Q & L~f /\ Q is closed &
P is_an_arc_of f/.1, f/.len f by A1,A2,TOPREAL1:31,TOPS_1:35;
then First_Point (P, f/.1, f/.len f, Q) in L~f /\ Q by Def1;
then A5: First_Point (P, f/.1, f/.len f, Q) in L~f &
First_Point (P, f/.1, f/.len f, Q) in Q by XBOOLE_0:def 3;
set FPO = First_Point (R, f/.i, f/.(i+1), Q),
FPG = First_Point (P, f/.1, f/.len f, Q);
A6: i in dom f & i+1 in dom f by A2,GOBOARD2:3;
A7: f/.i <> f/.(i+1)
proof
assume f/.i = f/.(i+1);
then i = i+1 by A3,A6,PARTFUN2:17;
hence thesis by REAL_1:69;
end;
FPG = FPO
proof
A8: LSeg (f,i) is closed by SPPOL_1:40;
A9:LSeg (f,i) = LSeg (f/.i, f/.(i+1)) by A2,TOPREAL1:def 5;
LSeg (f, i) /\ Q <> {} by A2,A5,XBOOLE_0:def 3;
then A10: LSeg (f, i) meets Q & LSeg (f, i) /\ Q is closed &
R is_an_arc_of f/.i, f/.(i+1)
by A2,A7,A8,A9,TOPREAL1:15,TOPS_1:35,XBOOLE_0:def 7;
FPG in L~f /\ Q &
for g being map of I[01], (TOP-REAL 2)|P, s2 be Real st
g is_homeomorphism & g.0=f/.1 & g.1=f/.len f
& g.s2= FPG
& 0<=s2 & s2<=1 holds (for t be Real st 0<=t & t<s2 holds not g.t in Q)
by A4,Def1;
then A11:FPG in L~f by XBOOLE_0:def 3;
consider F be map of I[01], (TOP-REAL 2)|P such that
A12: F is_homeomorphism & F.0 = f/.1 & F.1 = f/.len f
by A4,TOPREAL1:def 2;
A13:dom F = [#]I[01] by A12,TOPS_2:def 5
.= [.0,1.] by BORSUK_1:83,PRE_TOPC:12;
rng F = [#]((TOP-REAL 2)|P) by A12,TOPS_2:def 5
.= L~f by PRE_TOPC:def 10;
then consider s21 be set such that
A14: s21 in dom F & F.s21 = FPG by A11,FUNCT_1:def 5;
reconsider s21 as Real by A13,A14;
A15:0 <= s21 & s21 <= 1 by A13,A14,BORSUK_1:83,JORDAN5A:2;
A16: FPG in LSeg (f,i) /\ Q by A2,A5,XBOOLE_0:def 3;
for g being map of I[01], (TOP-REAL 2)|R, s2 be Real st
g is_homeomorphism & g.0=f/.i & g.1=f/.(i+1)
& g.s2 = FPG
& 0<=s2 & s2<=1 holds (for t be Real st 0<=t & t<s2 holds not g.t in Q)
proof
let g be map of I[01], (TOP-REAL 2)|R, s2 be Real;
assume A17: g is_homeomorphism & g.0=f/.i & g.1=f/.(i+1)
& g.s2 = FPG & 0<=s2 & s2<=1;
consider ppi, pi1 be Real such that
A18: ppi < pi1 & 0 <= ppi & ppi <= 1 & 0 <= pi1 & pi1 <= 1 &
LSeg (f, i) = F.:[.ppi, pi1.] & F.ppi = f/.i & F.pi1 = f/.(i+1)
by A2,A12,JORDAN5B:7;
A19: ppi in { dd where dd is Real : ppi <= dd & dd <= pi1 } &
pi1 in { dd where dd is Real : ppi <= dd & dd <= pi1 } by A18;
then A20: ppi in [.ppi,pi1.] & pi1 in [.ppi,pi1.] by RCOMP_1:def 1;
A21: [.ppi,pi1.] c= [.0,1.] by A18,TREAL_1:1;
then reconsider Poz = [.ppi, pi1.] as non empty Subset of I[01]
by A19,BORSUK_1:83,RCOMP_1:def 1;
the carrier of ((TOP-REAL 2)|P) = [#] ((TOP-REAL 2)|P) by PRE_TOPC:12
.= P by PRE_TOPC:def 10;
then reconsider SEG = LSeg (f, i) as non empty Subset of
the carrier of (TOP-REAL 2)|P by A2,TOPREAL3:26;
A22: the carrier of (((TOP-REAL 2) | P) | SEG) =
[#](((TOP-REAL 2) | P) | SEG) by PRE_TOPC:12
.= SEG by PRE_TOPC:def 10;
reconsider SE = SEG as non empty Subset of TOP-REAL 2;
reconsider SEG as non empty Subset of (TOP-REAL 2)|P;
A23: ((TOP-REAL 2) | P) | SEG = (TOP-REAL 2) | SE by GOBOARD9:4;
consider hh be map of I[01]|Poz, (TOP-REAL 2)|R such that
A24: hh = F|Poz & hh is_homeomorphism by A2,A12,A18,JORDAN5B:8;
A25: F is continuous & F is one-to-one by A12,TOPS_2:def 5;
A26: hh is one-to-one by A24,TOPS_2:def 5;
A27: hh is one-to-one by A24,TOPS_2:def 5;
A28: dom hh = [#] (I[01] | Poz) by A24,TOPS_2:def 5;
then A29:dom hh = Poz by PRE_TOPC:def 10;
A30:rng hh = hh.:(the carrier of (I[01]|Poz)) by FUNCT_2:45
.= hh.:(dom hh) by A28,PRE_TOPC:12
.= SEG by A18,A24,A29,RFUNCT_2:5
.= [#](((TOP-REAL 2) | P) | SEG) by A22,PRE_TOPC:12;
A31:the carrier of Closed-Interval-TSpace (ppi,pi1) = Poz by A18,TOPMETR:25;
reconsider A = Closed-Interval-TSpace (ppi,pi1) as
strict SubSpace of I[01] by A18,TOPMETR:27,TREAL_1:6;
A32:Poz = [#] A by A31,PRE_TOPC:12;
A33: rng g = [#]((TOP-REAL 2) | SE) by A17,TOPS_2:def 5;
A34: rng (hh") = [#] (I[01] | Poz) by A23,A26,A30,TOPS_2:62
.= Poz by PRE_TOPC:def 10;
set H = hh" * g;
A35: id Poz is one-to-one by FUNCT_1:52;
A36:hh = F * id Poz by A24,RELAT_1:94;
A37: dom g = [#]I[01] by A17,TOPS_2:def 5
.= the carrier of I[01] by PRE_TOPC:12;
let t be Real; assume A38: 0 <= t & t < s2;
then A39: t < 1 by A17,AXIOMS:22;
then A40: t in dom g by A37,A38,JORDAN5A:2;
ppi in dom F /\ Poz & pi1 in dom F /\ Poz by A13,A20,A21,XBOOLE_0:def 3
;
then A41: ppi in dom hh & pi1 in dom hh by A24,RELAT_1:90;
then A42: hh.ppi = f/.i & hh.pi1 = f/.(i+1) by A18,A24,FUNCT_1:70;
0 in dom g by A37,JORDAN5A:2;
then A43:H.0 = hh".(f/.i) by A17,FUNCT_1:23
.= (hh qua Function)".(f/.i) by A23,A27,A30,TOPS_2:def 4
.= ppi by A27,A41,A42,FUNCT_1:54;
1 in dom g by A37,JORDAN5A:2;
then A44: H.1 = hh".(f/.(i+1)) by A17,FUNCT_1:23
.= (hh qua Function)".(f/.(i+1)) by A23,A27,A30,TOPS_2:def 4
.= pi1 by A27,A41,A42,FUNCT_1:54;
set ss = H.t;
A45: dom (hh") = [#] (((TOP-REAL 2) | P) | SEG)
by A23,A26,A30,TOPS_2:62;
then A46: dom H = dom g & rng H = rng (hh") by A23,A33,RELAT_1:46,47;
A47: rng H = Poz by A23,A33,A34,A45,RELAT_1:47;
ss in Poz by A34,A40,A46,FUNCT_1:def 5;
then ss in { l where l is Real : ppi <= l & l <= pi1 } by RCOMP_1:def 1;
then consider ss' be Real such that
A48: ss' = ss & ppi <= ss' & ss' <= pi1;
A49: F is one-to-one by A12,TOPS_2:def 5;
A50: rng F = [#]((TOP-REAL 2)|P) by A12,TOPS_2:def 5;
g.t in [#] ((TOP-REAL 2) | SE) by A33,A40,FUNCT_1:def 5;
then A51: g.t in SEG by PRE_TOPC:def 10;
then g.t in the carrier of ((TOP-REAL 2)|P);
then A52: g.t in rng F by A50,PRE_TOPC:12;
A53: t in dom H by A23,A33,A40,A45,RELAT_1:46;
A54: g.t in dom (F") by A49,A50,A52,TOPS_2:62;
consider x be set such that
A55: x in dom F & x in Poz & g.t = F.x by A18,A51,FUNCT_1:def 12;
x = (F qua Function)".(g.t) by A25,A55,FUNCT_1:54;
then A56: F".(g.t) in Poz by A49,A50,A55,TOPS_2:def 4;
A57: (F qua Function)".(g.t) in Poz by A25,A55,FUNCT_1:54;
A58: F".(g.t) in dom (id Poz) by A56,FUNCT_1:34;
consider z be set such that
A59: z in dom F & z in Poz & F.s21 = F.z by A2,A14,A18,FUNCT_1:def 12;
A60:s21 in Poz by A14,A25,A59,FUNCT_1:def 8;
A61:s2 in dom g by A17,A37,JORDAN5A:2;
hh.s21 = g.s2 by A14,A17,A24,A60,FUNCT_1:72;
then s21 = (hh qua Function)".(g.s2) by A26,A29,A60,FUNCT_1:54;
then A62: s21 = hh".(g.s2) by A23,A26,A30,TOPS_2:def 4;
A63: dom H = the carrier of Closed-Interval-TSpace(0,1)
by A23,A33,A37,A45,RELAT_1:46,TOPMETR:27;
rng H c= the carrier of Closed-Interval-TSpace(ppi,pi1)
by A18,A47,TOPMETR:25;
then H is Function of the carrier of Closed-Interval-TSpace(0,1),
the carrier of Closed-Interval-TSpace(ppi,pi1)
by A63,FUNCT_2:4;
then reconsider H as map of Closed-Interval-TSpace(0,1),
Closed-Interval-TSpace(ppi,pi1);
reconsider w1 = s2, w2 = t as Point of Closed-Interval-TSpace(0,1)
by A17,A38,A39,JORDAN5A:2,TOPMETR:27;
A64: g is continuous one-to-one by A17,TOPS_2:def 5;
hh" is_homeomorphism by A24,TOPS_2:70;
then A65: hh" is continuous one-to-one by TOPS_2:def 5;
I[01] | Poz = A by A32,PRE_TOPC:def 10;
then A66: H is continuous one-to-one by A64,A65,FUNCT_1:46,TOPMETR:27,TOPS_2:58
;
s21 = H.w1 &
ss' = H.w2 & t < s2 & ppi < pi1 by A18,A38,A48,A61,A62,FUNCT_1:23;
then A67: ss' < s21 by A43,A44,A66,JORDAN5A:16;
F.ss = (((hh"*g) qua Relation) * (F qua Relation)).t by A53,FUNCT_1:23
.= ( (g qua Relation) * ((hh" qua Relation) * (F qua Relation))).t
by RELAT_1:55
.= (F*hh").(g.t) by A40,FUNCT_1:23
.= (F*(hh qua Function)").(g.t) by A23,A26,A30,TOPS_2:def 4
.= ( F * (((F qua Function)" qua Relation) *
((id Poz)" qua Relation))).(g.t) by A25,A35,A36,FUNCT_1:66
.= ( ((F" qua Relation) * ((id Poz)" qua Relation)) *
(F qua Relation)).(g.t) by A49,A50,TOPS_2:def 4
.= ( (F" qua Relation) * (((id Poz)" qua Relation) *
(F qua Relation))).(g.t) by RELAT_1:55
.= ( (F" qua Relation) * ((F*id Poz) qua Relation) ).(g.t) by FUNCT_1:67
.= (F*(id Poz)).(F".(g.t)) by A54,FUNCT_1:23
.= F.((id Poz).(F".(g.t))) by A58,FUNCT_1:23
.= F.((id Poz).((F qua Function)".(g.t))) by A49,A50,TOPS_2:def 4
.= F.((F qua Function)".(g.t)) by A57,FUNCT_1:34
.= g.t by A49,A52,FUNCT_1:57;
hence thesis by A4,A12,A14,A15,A18,A48,A67,Def1;
end;
hence thesis by A10,A16,Def1;
end;
hence thesis;
end;
theorem Th20:
for f being FinSequence of TOP-REAL 2,
Q being Subset of TOP-REAL 2,
i being Nat
st L~f meets Q & Q is closed & f is_S-Seq & 1 <= i & i+1 <= len f &
Last_Point (L~f, f/.1, f/.len f, Q) in LSeg (f, i) holds
Last_Point (L~f, f/.1, f/.len f, Q) =
Last_Point (LSeg (f, i), f/.i, f/.(i+1), Q)
proof
let f be FinSequence of TOP-REAL 2,
Q be Subset of TOP-REAL 2,
i be Nat;
A1: L~f is closed by SPPOL_1:49;
assume A2: L~f meets Q & Q is closed & f is_S-Seq & 1 <= i & i+1 <= len f &
Last_Point (L~f, f/.1, f/.len f, Q) in LSeg (f, i);
then A3: f is one-to-one by TOPREAL1:def 10;
len f >= 2 by A2,TOPREAL1:def 10;
then reconsider P = L~f, R = LSeg (f, i) as non empty
Subset of TOP-REAL 2 by A2,TOPREAL1:29;
A4: L~f meets Q & L~f /\ Q is closed &
P is_an_arc_of f/.1, f/.len f by A1,A2,TOPREAL1:31,TOPS_1:35;
then Last_Point (P, f/.1, f/.len f, Q) in L~f /\ Q by Def2;
then A5: Last_Point (P, f/.1, f/.len f, Q) in L~f &
Last_Point (P, f/.1, f/.len f, Q) in Q by XBOOLE_0:def 3;
set FPO = Last_Point (R, f/.i, f/.(i+1), Q),
FPG = Last_Point (P, f/.1, f/.len f, Q);
A6: i in dom f & i+1 in dom f by A2,GOBOARD2:3;
A7: f/.i <> f/.(i+1)
proof
assume f/.i = f/.(i+1);
then i = i+1 by A3,A6,PARTFUN2:17;
hence thesis by REAL_1:69;
end;
FPG = FPO
proof
A8: LSeg (f,i) is closed by SPPOL_1:40;
A9:LSeg (f,i) = LSeg (f/.i, f/.(i+1)) by A2,TOPREAL1:def 5;
LSeg (f, i) /\ Q <> {} by A2,A5,XBOOLE_0:def 3;
then A10: LSeg (f, i) meets Q & LSeg (f, i) /\ Q is closed &
R is_an_arc_of f/.i, f/.(i+1)
by A2,A7,A8,A9,TOPREAL1:15,TOPS_1:35,XBOOLE_0:def 7;
FPG in L~f /\ Q &
for g being map of I[01], (TOP-REAL 2)|P, s2 be Real st
g is_homeomorphism & g.0=f/.1 & g.1=f/.len f
& g.s2= FPG
& 0<=s2 & s2<=1 holds (for t be Real st 1>=t & t>s2 holds not g.t in Q)
by A4,Def2;
then A11:FPG in L~f by XBOOLE_0:def 3;
consider F be map of I[01], (TOP-REAL 2)|P such that
A12: F is_homeomorphism & F.0 = f/.1 & F.1 = f/.len f
by A4,TOPREAL1:def 2;
A13:dom F = [#]I[01] by A12,TOPS_2:def 5
.= [.0,1.] by BORSUK_1:83,PRE_TOPC:12;
rng F = [#]((TOP-REAL 2)|P) by A12,TOPS_2:def 5
.= L~f by PRE_TOPC:def 10;
then consider s21 be set such that
A14: s21 in dom F & F.s21 = FPG by A11,FUNCT_1:def 5;
reconsider s21 as Real by A13,A14;
A15:0 <= s21 & s21 <= 1 by A13,A14,BORSUK_1:83,JORDAN5A:2;
A16: FPG in LSeg (f,i) /\ Q by A2,A5,XBOOLE_0:def 3;
for g being map of I[01], (TOP-REAL 2)|R, s2 be Real st
g is_homeomorphism & g.0=f/.i & g.1=f/.(i+1)
& g.s2 = FPG
& 0<=s2 & s2<=1 holds (for t be Real st 1>=t & t>s2 holds not g.t in Q)
proof
let g be map of I[01], (TOP-REAL 2)|R, s2 be Real;
assume A17: g is_homeomorphism & g.0=f/.i & g.1=f/.(i+1)
& g.s2 = FPG & 0<=s2 & s2<=1;
consider ppi, pi1 be Real such that
A18: ppi < pi1 & 0 <= ppi & ppi <= 1 & 0 <= pi1 & pi1 <= 1 &
LSeg (f, i) = F.:[.ppi, pi1.] & F.ppi = f/.i & F.pi1 = f/.(i+1)
by A2,A12,JORDAN5B:7;
A19: ppi in { dd where dd is Real : ppi <= dd & dd <= pi1 } &
pi1 in { dd where dd is Real : ppi <= dd & dd <= pi1 } by A18;
then A20: ppi in [.ppi,pi1.] & pi1 in [.ppi,pi1.] by RCOMP_1:def 1;
A21: [.ppi,pi1.] c= [.0,1.] by A18,TREAL_1:1;
then reconsider Poz = [.ppi, pi1.] as non empty Subset of I[01]
by A19,BORSUK_1:83,RCOMP_1:def 1;
A22: the carrier of (I[01]|Poz) = [#] (I[01]|Poz) by PRE_TOPC:12
.= Poz by PRE_TOPC:def 10;
set gg = F | Poz;
gg is Function of the carrier of (I[01]|Poz),
the carrier of (TOP-REAL 2)| P by A22,FUNCT_2:38;
then reconsider gg as map of I[01]|Poz, (TOP-REAL 2)| P;
reconsider Lf = L~f as non empty Subset of TOP-REAL 2
by A4;
the carrier of ((TOP-REAL 2)|Lf) = [#] ((TOP-REAL 2)|Lf) by PRE_TOPC:12
.= Lf by PRE_TOPC:def 10;
then reconsider SEG = LSeg (f, i)
as non empty Subset of (TOP-REAL 2)|Lf
by A2,TOPREAL3:26;
A23: the carrier of (((TOP-REAL 2) | Lf) | SEG) =
[#](((TOP-REAL 2) | Lf) | SEG) by PRE_TOPC:12
.= SEG by PRE_TOPC:def 10;
rng gg c= SEG
proof
let ii be set; assume ii in rng gg;
then consider j be set such that
A24: j in dom gg & ii = gg.j by FUNCT_1:def 5;
j in dom F /\ Poz by A24,RELAT_1:90;
then A25: j in dom F by XBOOLE_0:def 3;
A26: dom gg = Poz by A22,FUNCT_2:def 1;
then j in dom F & F.j in LSeg (f,i) by A18,A24,A25,FUNCT_1:def 12;
hence thesis by A24,A26,FUNCT_1:72;
end;
then A27:gg is Function of the carrier of (I[01]|Poz), the carrier of
(((TOP-REAL 2) | Lf) | SEG) by A23,FUNCT_2:8;
reconsider SE = SEG as non empty Subset of TOP-REAL 2;
reconsider SEG as non empty Subset of (TOP-REAL 2)|Lf;
A28: ((TOP-REAL 2) | Lf) | SEG = (TOP-REAL 2) | SE by GOBOARD9:4;
reconsider hh' = gg as map of I[01]|Poz, ((TOP-REAL 2) | Lf)| SEG
by A27;
A29: F is continuous & F is one-to-one by A12,TOPS_2:def 5;
then gg is continuous by TOPMETR:10;
then A30: hh' is continuous by TOPMETR:9;
A31: hh' is one-to-one by A29,FUNCT_1:84;
reconsider hh = hh' as map of I[01]|Poz, (TOP-REAL 2) | SE
by A28;
A32: hh is one-to-one by A29,FUNCT_1:84;
A33: dom hh = the carrier of (I[01] | Poz) by FUNCT_2:def 1
.= [#] (I[01] | Poz) by PRE_TOPC:12;
then A34:dom hh = Poz by PRE_TOPC:def 10;
A35:rng hh = hh.:(the carrier of (I[01]|Poz)) by FUNCT_2:45
.= hh.:(dom hh) by A33,PRE_TOPC:12
.= SEG by A18,A34,RFUNCT_2:5
.= [#](((TOP-REAL 2) | Lf) | SEG) by A23,PRE_TOPC:12;
A36:the carrier of Closed-Interval-TSpace (ppi,pi1) = Poz by A18,TOPMETR:25;
reconsider A = Closed-Interval-TSpace (ppi,pi1) as
strict SubSpace of I[01] by A18,TOPMETR:27,TREAL_1:6;
A37:Poz = [#] A by A36,PRE_TOPC:12;
Closed-Interval-TSpace (ppi,pi1) is compact by A18,HEINE:11;
then [#] Closed-Interval-TSpace (ppi,pi1) is compact by COMPTS_1:10;
then for P being Subset of A st P=Poz holds P is compact by A36,PRE_TOPC:12
;
then Poz is compact by A37,COMPTS_1:11;
then A38: I[01]|Poz is compact by COMPTS_1:12;
TOP-REAL 2 is_T2 by SPPOL_1:26;
then (TOP-REAL 2)|SE is_T2 by TOPMETR:3;
then A39: hh is_homeomorphism by A28,A30,A31,A33,A35,A38,COMPTS_1:26;
A40: rng g = [#]((TOP-REAL 2) | SE) by A17,TOPS_2:def 5;
A41: rng (hh") = [#] (I[01] | Poz) by A28,A31,A35,TOPS_2:62
.= Poz by PRE_TOPC:def 10;
set H = hh" * g;
A42: id Poz is one-to-one by FUNCT_1:52;
A43:hh = F * id Poz by RELAT_1:94;
A44: dom g = [#]I[01] by A17,TOPS_2:def 5
.= the carrier of I[01] by PRE_TOPC:12;
let t be Real; assume A45: 1 >= t & t > s2;
then A46: t > 0 by A17;
then A47: t in dom g by A44,A45,JORDAN5A:2;
ppi in dom F /\ Poz & pi1 in dom F /\ Poz by A13,A20,A21,XBOOLE_0:def 3
;
then A48: ppi in dom hh & pi1 in dom hh by RELAT_1:90;
then A49: hh.ppi = f/.i & hh.pi1 = f/.(i+1) by A18,FUNCT_1:70;
0 in dom g by A44,JORDAN5A:2;
then A50:H.0 = hh".(f/.i) by A17,FUNCT_1:23
.= (hh qua Function)".(f/.i) by A28,A32,A35,TOPS_2:def 4
.= ppi by A32,A48,A49,FUNCT_1:54;
1 in dom g by A44,JORDAN5A:2;
then A51: H.1 = hh".(f/.(i+1)) by A17,FUNCT_1:23
.= (hh qua Function)".(f/.(i+1)) by A28,A32,A35,TOPS_2:def 4
.= pi1 by A32,A48,A49,FUNCT_1:54;
set ss = H.t;
A52: dom (hh") = [#] (((TOP-REAL 2) | Lf) | SEG)
by A28,A31,A35,TOPS_2:62;
then A53: dom H = dom g & rng H = rng (hh") by A28,A40,RELAT_1:46,47;
A54: rng H = Poz by A28,A40,A41,A52,RELAT_1:47;
ss in Poz by A41,A47,A53,FUNCT_1:def 5;
then ss in { l where l is Real : ppi <= l & l <= pi1 } by RCOMP_1:def 1;
then consider ss' be Real such that
A55: ss' = ss & ppi <= ss' & ss' <= pi1;
A56: F is one-to-one by A12,TOPS_2:def 5;
A57: rng F = [#]((TOP-REAL 2)|P) by A12,TOPS_2:def 5;
g.t in [#] ((TOP-REAL 2) | SE) by A40,A47,FUNCT_1:def 5;
then A58: g.t in SEG by PRE_TOPC:def 10;
then g.t in the carrier of ((TOP-REAL 2)|Lf);
then A59: g.t in rng F by A57,PRE_TOPC:12;
A60: t in dom H by A28,A40,A47,A52,RELAT_1:46;
A61: g.t in dom (F") by A56,A57,A59,TOPS_2:62;
consider x be set such that
A62: x in dom F & x in Poz & g.t = F.x by A18,A58,FUNCT_1:def 12;
x = (F qua Function)".(g.t) by A29,A62,FUNCT_1:54;
then A63: F".(g.t) in Poz by A56,A57,A62,TOPS_2:def 4;
A64: (F qua Function)".(g.t) in Poz by A29,A62,FUNCT_1:54;
A65: F".(g.t) in dom (id Poz) by A63,FUNCT_1:34;
consider z be set such that
A66: z in dom F & z in Poz & F.s21 = F.z by A2,A14,A18,FUNCT_1:def 12;
A67:s21 in Poz by A14,A29,A66,FUNCT_1:def 8;
A68:s2 in dom g by A17,A44,JORDAN5A:2;
hh.s21 = g.s2 by A14,A17,A67,FUNCT_1:72;
then s21 = (hh qua Function)".(g.s2) by A31,A34,A67,FUNCT_1:54;
then A69: s21 = hh".(g.s2) by A28,A31,A35,TOPS_2:def 4;
A70: dom H = the carrier of Closed-Interval-TSpace(0,1)
by A28,A40,A44,A52,RELAT_1:46,TOPMETR:27;
rng H c= the carrier of Closed-Interval-TSpace(ppi,pi1)
by A18,A54,TOPMETR:25;
then H is Function of the carrier of Closed-Interval-TSpace(0,1),
the carrier of Closed-Interval-TSpace(ppi,pi1)
by A70,FUNCT_2:4;
then reconsider H as map of Closed-Interval-TSpace(0,1),
Closed-Interval-TSpace(ppi,pi1);
reconsider w1 = s2, w2 = t as Point of Closed-Interval-TSpace(0,1)
by A17,A45,A46,JORDAN5A:2,TOPMETR:27;
A71: g is continuous one-to-one by A17,TOPS_2:def 5;
hh" is_homeomorphism by A39,TOPS_2:70;
then A72: hh" is continuous one-to-one by TOPS_2:def 5;
I[01] | Poz = A by A37,PRE_TOPC:def 10;
then A73: H is continuous one-to-one by A71,A72,FUNCT_1:46,TOPMETR:27,TOPS_2:58
;
s21 = H.w1 &
ss' = H.w2 & t > s2 & ppi < pi1 by A18,A45,A55,A68,A69,FUNCT_1:23;
then A74: ss' > s21 by A50,A51,A73,JORDAN5A:16;
A75: 1 >= ss' by A18,A55,AXIOMS:22;
F.ss = (((hh"*g) qua Relation) * (F qua Relation)).t by A60,FUNCT_1:23
.= ( (g qua Relation) * ((hh" qua Relation) * (F qua Relation))).t
by RELAT_1:55
.= (F*hh").(g.t) by A47,FUNCT_1:23
.= (F*(hh qua Function)").(g.t) by A28,A31,A35,TOPS_2:def 4
.= ( F * (((F qua Function)" qua Relation) *
((id Poz)" qua Relation))).(g.t) by A29,A42,A43,FUNCT_1:66
.= ( ((F" qua Relation) * ((id Poz)" qua Relation)) *
(F qua Relation)).(g.t) by A56,A57,TOPS_2:def 4
.= ( (F" qua Relation) * (((id Poz)" qua Relation) *
(F qua Relation))).(g.t) by RELAT_1:55
.= ( (F" qua Relation) * ((F*id Poz) qua Relation) ).(g.t) by FUNCT_1:67
.= (F*(id Poz)).(F".(g.t)) by A61,FUNCT_1:23
.= F.((id Poz).(F".(g.t))) by A65,FUNCT_1:23
.= F.((id Poz).((F qua Function)".(g.t))) by A56,A57,TOPS_2:def 4
.= F.((F qua Function)".(g.t)) by A64,FUNCT_1:34
.= g.t by A56,A59,FUNCT_1:57;
hence thesis by A4,A12,A14,A15,A55,A74,A75,Def2;
end;
hence thesis by A10,A16,Def2;
end;
hence thesis;
end;
theorem
for f being FinSequence of TOP-REAL 2,
i be Nat st 1 <= i & i+1 <= len f & f is_S-Seq &
First_Point (L~f, f/.1, f/.len f, LSeg (f,i) ) in LSeg (f,i) holds
First_Point (L~f, f/.1, f/.len f, LSeg (f,i) ) = f/.i
proof
let f be FinSequence of TOP-REAL 2,
i be Nat;
assume A1: 1 <= i & i+1 <= len f & f is_S-Seq &
First_Point ( L~f, f/.1, f/.len f, LSeg (f,i) ) in LSeg (f,i);
then reconsider Q = LSeg (f,i)
as non empty Subset of TOP-REAL 2;
Q = LSeg (f/.i, f/.(i+1)) by A1,TOPREAL1:def 5;
then Q c= L~f by A1,SPPOL_2:16;
then L~f meets Q & Q is closed by A1,SPPOL_1:40,XBOOLE_0:3;
then A2: First_Point (L~f, f/.1, f/.len f, Q) =
First_Point (Q, f/.i, f/.(i+1), Q) by A1,Th19;
Q is closed & Q is_an_arc_of f/.i, f/.(i+1)
by A1,JORDAN5B:15,SPPOL_1:40;
hence thesis by A2,Th7;
end;
theorem
for f being FinSequence of TOP-REAL 2,
i be Nat st 1 <= i & i+1 <= len f & f is_S-Seq &
Last_Point ( L~f, f/.1, f/.len f, LSeg (f,i) ) in LSeg (f,i)
holds
Last_Point ( L~f, f/.1, f/.len f, LSeg (f,i) ) = f/.(i+1)
proof
let f be FinSequence of TOP-REAL 2,
i be Nat;
assume A1: 1 <= i & i+1 <= len f & f is_S-Seq &
Last_Point ( L~f, f/.1, f/.len f, LSeg (f,i) ) in LSeg (f,i);
then reconsider Q = LSeg (f,i)
as non empty Subset of TOP-REAL 2;
Q = LSeg (f/.i, f/.(i+1)) by A1,TOPREAL1:def 5;
then Q c= L~f by A1,SPPOL_2:16;
then L~f meets Q & Q is closed by A1,SPPOL_1:40,XBOOLE_0:3;
then A2: Last_Point (L~f, f/.1, f/.len f, Q) =
Last_Point (Q, f/.i, f/.(i+1), Q) by A1,Th20;
Q is closed & Q is_an_arc_of f/.i, f/.(i+1)
by A1,JORDAN5B:15,SPPOL_1:40;
hence thesis by A2,Th7;
end;
theorem Th23:
for f be FinSequence of TOP-REAL 2,
i be Nat st
f is_S-Seq & 1 <= i & i+1 <= len f holds
LE f/.i, f/.(i+1), L~f, f/.1, f/.len f
proof
let f be FinSequence of TOP-REAL 2,
i be Nat;
assume
A1: f is_S-Seq & 1 <= i & i+1 <= len f;
set p1 = f/.1, p2 = f/.len f, q1 = f/.i, q2 = f/.(i+1);
A2:len f >= 2 by A1,TOPREAL1:def 10;
then reconsider P = L~f as non empty Subset of TOP-REAL 2
by TOPREAL1:29;
A3:i in dom f & i+1 in dom f by A1,GOBOARD2:3;
then A4: q1 in P by A2,GOBOARD1:16;
A5: q2 in P by A2,A3,GOBOARD1:16;
for g being map of I[01], (TOP-REAL 2)|P, s1,s2 be Real st
g is_homeomorphism & g.0=p1 & g.1=p2 & g.s1=q1 & 0<=s1 & s1<=1 &
g.s2=q2 & 0<=s2 & s2<=1 holds s1<=s2
proof
let g be map of I[01], (TOP-REAL 2)|P, s1,s2 be Real;
assume
A6: g is_homeomorphism & g.0 = p1 & g.1 = p2 & g.s1 = q1 &
0 <= s1 & s1 <= 1 & g.s2 = q2 & 0 <= s2 & s2 <= 1;
then consider r1, r2 be Real such that
A7: r1 < r2 & 0 <= r1 & r1 <= 1 & 0 <= r2 & r2 <= 1 &
LSeg (f, i) = g.:[.r1, r2.] & g.r1 = q1 & g.r2 = q2 by A1,JORDAN5B:7;
dom g = [#]I[01] by A6,TOPS_2:def 5
.= the carrier of I[01] by PRE_TOPC:12;
then A8: r1 in dom g & s1 in dom g & r2 in dom g & s2 in dom g by A6,A7,
JORDAN5A:2;
g is one-to-one by A6,TOPS_2:def 5;
then s1 = r1 & s2 = r2 by A6,A7,A8,FUNCT_1:def 8;
hence thesis by A7;
end;
hence thesis by A4,A5,Def3;
end;
theorem Th24:
for f be FinSequence of TOP-REAL 2,
i, j be Nat st
f is_S-Seq & 1 <= i & i <= j & j <= len f holds
LE f/.i, f/.j, L~f, f/.1, f/.len f
proof
let f be FinSequence of TOP-REAL 2,
i, j be Nat such that
A1: f is_S-Seq and
A2: 1 <= i and
A3: i <= j and
A4: j <= len f;
A5: len f >= 2 by A1,TOPREAL1:def 10;
then reconsider P = L~f as non empty Subset of TOP-REAL 2
by TOPREAL1:29;
consider k being Nat such that
A6: i+k = j by A3,NAT_1:28;
A7: P is_an_arc_of f/.1, f/.len f by A1,TOPREAL1:31;
defpred ILE[Nat] means
1 <= i & i+$1 <= len f implies
LE f/.i, f/.(i+$1), P, f/.1, f/.len f;
A8: ILE[0]
proof
assume 1 <= i & i+0 <= len f;
then i in dom f by FINSEQ_3:27;
then f/.i in P by A5,GOBOARD1:16;
hence thesis by A7,Th9;
end;
A9: for l be Nat st ILE[l] holds ILE[l + 1]
proof
let l be Nat; assume A10: ILE[l];
A11: i <= i+l by NAT_1:29;
assume A12: 1 <= i & i+(l+1) <= len f;
A13: f/.(i+l+1) = f/.(i+(l+1)) by XCMPLX_1:1;
1 <= i+l & i+l+1 <= len f by A11,A12,AXIOMS:22,XCMPLX_1:1;
then A14: LE f/.(i+l), f/.(i+(l+1)), P, f/.1,f/.len f by A1,A13,Th23;
A15: i+(l+1) = i+l+1 by XCMPLX_1:1;
i+l <= i+l+1 by NAT_1:29;
hence thesis by A7,A10,A12,A14,A15,Th13,AXIOMS:22;
end;
for l be Nat holds ILE[l] from Ind(A8, A9);
hence thesis by A2,A4,A6;
end;
Lm2:
for f being FinSequence of TOP-REAL 2,
Q being Subset of TOP-REAL 2,
q being Point of TOP-REAL 2,
i being Nat st
LSeg (f,i) meets Q & f is_S-Seq & Q is closed &
1<=i & i+1<=len f & q in LSeg(f,i) & q in Q holds
LE First_Point(LSeg(f,i), f/.i,f/.(i+1),Q), q, f/.i, f/.(i+1)
proof
let f be FinSequence of TOP-REAL 2,
Q be Subset of TOP-REAL 2,
q be Point of TOP-REAL 2,
i be Nat;
assume A1: LSeg(f,i) meets Q & f is_S-Seq & Q is closed &
1<=i & i+1<=len f & q in LSeg(f,i) & q in Q;
then A2: LSeg(f,i) = LSeg(f/.i, f/.(i+1)) by TOPREAL1:def 5;
reconsider P = LSeg(f,i) as non empty Subset of TOP-REAL 2
by A1;
P is closed by SPPOL_1:40;
then A3: P /\ Q is closed by A1,TOPS_1:35;
A4: P is_an_arc_of f/.i,f/.(i+1) by A1,JORDAN5B:15;
A5: P /\ Q c= P by XBOOLE_1:17;
set q1 = First_Point(P,f/.i,f/.(i+1),Q), p1 = f/.i, p2 = f/.(i+1);
A6: f is one-to-one by A1,TOPREAL1:def 10;
A7: i in dom f & i+1 in dom f by A1,GOBOARD2:3;
A8: p1 <> p2
proof
assume p1 = p2;
then i = i+1 by A6,A7,PARTFUN2:17;
hence thesis by REAL_1:69;
end;
A9: q1 in P /\ Q by A1,A3,A4,Def1;
for g being map of I[01], (TOP-REAL 2)|P, s1, s2 be Real st
g is_homeomorphism
& g.0=p1 & g.1=p2
& g.s1=q1 & 0<=s1 & s1<=1
& g.s2=q & 0<=s2 & s2<=1
holds s1<=s2 by A1,A3,A4,Def1;
then LE q1, q, P, p1, p2 by A1,A5,A9,Def3;
hence thesis by A2,A8,Th17;
end;
Lm3:
for f being FinSequence of TOP-REAL 2,
Q being Subset of TOP-REAL 2,
q being Point of TOP-REAL 2,
i being Nat st
L~f meets Q & f is_S-Seq & Q is closed &
First_Point(L~f,f/.1,f/.len f,Q) in LSeg(f,i) & 1<=i & i+1<=len f &
q in LSeg(f,i) & q in Q holds
LE First_Point(L~f,f/.1,f/.len f,Q), q, f/.i, f/.(i+1)
proof
let f be FinSequence of TOP-REAL 2,
Q be Subset of TOP-REAL 2,
q be Point of TOP-REAL 2,
i be Nat;
assume A1: L~f meets Q & f is_S-Seq & Q is closed &
First_Point(L~f,f/.1,f/.len f,Q) in LSeg(f,i) & 1<=i & i+1<=len f &
q in LSeg(f,i) & q in Q;
then LSeg (f,i) /\ Q <> {} by XBOOLE_0:def 3;
then A2: LSeg (f,i) meets Q by XBOOLE_0:def 7;
len f >= 2 by A1,TOPREAL1:def 10;
then reconsider P = L~f, R = LSeg (f,i)
as non empty Subset of TOP-REAL 2 by A1,TOPREAL1:29;
First_Point (P,f/.1,f/.len f,Q) =
First_Point (R, f/.i, f/.(i+1), Q) by A1,Th19;
hence thesis by A1,A2,Lm2;
end;
Lm4:
for f being FinSequence of TOP-REAL 2,
Q being Subset of TOP-REAL 2,
q being Point of TOP-REAL 2,
i being Nat st
LSeg (f,i) meets Q & f is_S-Seq & Q is closed &
1<=i & i+1<=len f & q in LSeg(f,i) & q in Q holds
LE q, Last_Point(LSeg(f,i),f/.i,f/.(i+1),Q), f/.i, f/.(i+1)
proof
let f be FinSequence of TOP-REAL 2,
Q be Subset of TOP-REAL 2,
q be Point of TOP-REAL 2,
i be Nat;
assume A1: LSeg(f,i) meets Q & f is_S-Seq & Q is closed &
1<=i & i+1<=len f & q in LSeg(f,i) & q in Q;
then A2: LSeg(f,i) = LSeg(f/.i, f/.(i+1)) by TOPREAL1:def 5;
reconsider P = LSeg(f,i) as non empty Subset of TOP-REAL 2
by A1;
P is closed by SPPOL_1:40;
then A3: P /\ Q is closed by A1,TOPS_1:35;
A4: P is_an_arc_of f/.i,f/.(i+1) by A1,JORDAN5B:15;
A5: P /\ Q c= P by XBOOLE_1:17;
set q1 = Last_Point(P,f/.i,f/.(i+1),Q), p1 = f/.i, p2 = f/.(i+1);
A6: f is one-to-one by A1,TOPREAL1:def 10;
A7: i in dom f & i+1 in dom f by A1,GOBOARD2:3;
A8: p1 <> p2
proof
assume p1 = p2;
then i = i+1 by A6,A7,PARTFUN2:17;
hence thesis by REAL_1:69;
end;
A9: q1 in P /\ Q by A1,A3,A4,Def2;
for g being map of I[01], (TOP-REAL 2)|P, s1, s2 be Real st
g is_homeomorphism
& g.0=p1 & g.1=p2
& g.s1=q & 0<=s1 & s1<=1
& g.s2=q1 & 0<=s2 & s2<=1
holds s1<=s2 by A1,A3,A4,Def2;
then LE q, q1, P, p1, p2 by A1,A5,A9,Def3;
hence thesis by A2,A8,Th17;
end;
Lm5:
for f being FinSequence of TOP-REAL 2,
Q being Subset of TOP-REAL 2,
q being Point of TOP-REAL 2,
i being Nat st
L~f meets Q & f is_S-Seq & Q is closed &
Last_Point (L~f,f/.1,f/.len f,Q) in LSeg(f,i) &
1 <= i & i+1 <= len f &
q in LSeg(f,i) & q in Q holds
LE q, Last_Point(L~f,f/.1,f/.len f,Q), f/.i, f/.(i+1)
proof
let f be FinSequence of TOP-REAL 2,
Q be Subset of TOP-REAL 2,
q be Point of TOP-REAL 2,
i be Nat;
assume A1: L~f meets Q & f is_S-Seq & Q is closed &
Last_Point(L~f,f/.1,f/.len f,Q) in LSeg(f,i) & 1<=i & i+1<=len f &
q in LSeg(f,i) & q in Q;
then LSeg (f,i) /\ Q <> {} by XBOOLE_0:def 3;
then A2: LSeg (f,i) meets Q by XBOOLE_0:def 7;
len f >= 2 by A1,TOPREAL1:def 10;
then reconsider P = L~f, R = LSeg (f,i) as non empty Subset of the carrier
of TOP-REAL 2 by A1,TOPREAL1:29;
Last_Point(P,f/.1,f/.len f,Q) =
Last_Point (R, f/.i, f/.(i+1), Q) by A1,Th20;
hence thesis by A1,A2,Lm4;
end;
theorem Th25:
for f being FinSequence of TOP-REAL 2,
q being Point of TOP-REAL 2,
i being Nat st
f is_S-Seq & 1 <= i & i+1 <= len f & q in LSeg(f,i) holds
LE f/.i, q, L~f, f/.1, f/.len f
proof
let f be FinSequence of TOP-REAL 2,
q be Point of TOP-REAL 2,
i be Nat;
assume A1: f is_S-Seq & 1<=i & i+1<=len f & q in LSeg(f,i);
then A2: 2 <= len f by TOPREAL1:def 10;
then reconsider P = L~f as non empty Subset of the carrier
of TOP-REAL 2 by TOPREAL1:29;
set p1 = f/.1, p2 = f/.len f, q1 = f/.i;
i in dom f by A1,GOBOARD2:3;
then A3: q1 in P by A2,GOBOARD1:16;
A4: q in P by A1,SPPOL_2:17;
for g being map of I[01], (TOP-REAL 2)|P, s1,s2 be Real st
g is_homeomorphism
& g.0=p1 & g.1=p2 & g.s1=q1 & 0<=s1 & s1<=1 & g.s2=q & 0<=s2 & s2<=1
holds s1<=s2
proof
let g be map of I[01], (TOP-REAL 2)|P, s1,s2 be Real;
assume A5: g is_homeomorphism
& g.0=p1 & g.1=p2 & g.s1=q1 & 0<=s1 & s1<=1 & g.s2=q & 0<=s2 & s2<=1;
then consider r1, r2 be Real such that
A6: r1 < r2 & 0 <= r1 & r1 <= 1 & 0 <= r2 & r2 <= 1 &
LSeg (f, i) = g.:
[.r1, r2.] & g.r1 = q1 & g.r2 = f/.(i+1) by A1,JORDAN5B:7
;
consider r3' be set such that
A7: r3' in dom g & r3' in [.r1, r2.] & g.r3' = q by A1,A6,FUNCT_1:def 12;
r3' in { l where l is Real : r1 <= l & l <= r2 } by A7,RCOMP_1:def 1;
then consider r3 be Real such that
A8: r3 = r3' & r1 <= r3 & r3 <= r2;
dom g = [#]I[01] by A5,TOPS_2:def 5
.= the carrier of I[01] by PRE_TOPC:12;
then A9: r1 in dom g & s1 in dom g & r2 in dom g & s2 in dom g
by A5,A6,JORDAN5A:2;
A10: g is one-to-one by A5,TOPS_2:def 5;
then s2 = r3 by A5,A7,A8,A9,FUNCT_1:def 8;
hence thesis by A5,A6,A8,A9,A10,FUNCT_1:def 8;
end;
hence thesis by A3,A4,Def3;
end;
theorem Th26:
for f being FinSequence of TOP-REAL 2,
q being Point of TOP-REAL 2,
i being Nat st
f is_S-Seq & 1<=i & i+1<=len f & q in LSeg(f,i) holds
LE q, f/.(i+1), L~f, f/.1, f/.len f
proof
let f be FinSequence of TOP-REAL 2,
q be Point of TOP-REAL 2,
i be Nat;
assume A1: f is_S-Seq & 1<=i & i+1<=len f & q in LSeg(f,i);
then len f >= 2 by TOPREAL1:def 10;
then reconsider P = L~f as non empty Subset of the carrier
of TOP-REAL 2 by TOPREAL1:29;
set p1 = f/.1, p2 = f/.len f, q1 = f/.(i+1);
A2: q1 in LSeg (f,i) by A1,TOPREAL1:27;
A3: q in P by A1,SPPOL_2:17;
A4: q1 in P by A2,SPPOL_2:17;
for g being map of I[01], (TOP-REAL 2)|P, s1,s2 be Real st
g is_homeomorphism
& g.0=p1 & g.1=p2 & g.s1=q & 0<=s1 & s1<=1 & g.s2=q1 & 0<=s2 & s2<=1
holds s1<=s2
proof
let g be map of I[01], (TOP-REAL 2)|P, s1,s2 be Real;
assume A5: g is_homeomorphism
& g.0=p1 & g.1=p2 & g.s1=q & 0<=s1 & s1<=1 & g.s2=q1 & 0<=s2 & s2<=1;
then consider r1, r2 be Real such that
A6: r1 < r2 & 0 <= r1 & r1 <= 1 & 0 <= r2 & r2 <= 1 &
LSeg (f, i) = g.:[.r1, r2.] & g.r1 = f/.i & g.r2 = q1 by A1,JORDAN5B:7;
consider r3' be set such that
A7: r3' in dom g & r3' in [.r1, r2.] & g.r3' = q by A1,A6,FUNCT_1:def 12;
r3' in { l where l is Real : r1 <= l & l <= r2 } by A7,RCOMP_1:def 1;
then consider r3 be Real such that
A8: r3 = r3' & r1 <= r3 & r3 <= r2;
dom g = [#]I[01] by A5,TOPS_2:def 5
.= the carrier of I[01] by PRE_TOPC:12;
then A9: r1 in dom g & s1 in dom g & r2 in dom g & s2 in dom g by A5,A6,
JORDAN5A:2;
A10: g is one-to-one by A5,TOPS_2:def 5;
then s1 = r3 by A5,A7,A8,A9,FUNCT_1:def 8;
hence thesis by A5,A6,A8,A9,A10,FUNCT_1:def 8;
end;
hence thesis by A3,A4,Def3;
end;
theorem
for f being FinSequence of TOP-REAL 2,
Q being Subset of TOP-REAL 2,
q being Point of TOP-REAL 2,
i, j being Nat st
L~f meets Q & f is_S-Seq & Q is closed &
First_Point (L~f,f/.1,f/.len f,Q) in LSeg(f,i) & 1<=i & i+1<=len f &
q in LSeg(f,j) & 1 <= j & j + 1 <= len f & q in Q &
First_Point (L~f,f/.1,f/.len f,Q) <> q
holds
i <= j &
(i=j implies LE First_Point(L~f,f/.1,f/.len f,Q), q, f/.i, f/.(i+1))
proof
let f be FinSequence of TOP-REAL 2,
Q be Subset of TOP-REAL 2,
q be Point of TOP-REAL 2, i,j be Nat;
assume A1: L~f meets Q & f is_S-Seq & Q is closed
& First_Point(L~f,f/.1,f/.len f,Q) in LSeg(f,i) & 1<=i & i+1<=len f
& q in LSeg(f,j) & 1<=j & j+1<=len f & q in Q
& First_Point (L~f,f/.1,f/.len f,Q) <> q;
then A2: q in L~f by SPPOL_2:17;
reconsider P = L~f as non empty Subset of TOP-REAL 2 by A1,SPPOL_2:17;
set q1 = First_Point(P,f/.1,f/.len f,Q), p1 = f/.i;
A3: P is_an_arc_of f/.1, f/.len f by A1,TOPREAL1:31;
thus i <= j
proof
assume j < i;
then A4: j+1 <= i by NAT_1:38;
i <= i + 1 & j <= j + 1 by NAT_1:29;
then i <= len f & 1 <= j+1 by A1,AXIOMS:22;
then A5: LE f/.(j+1), p1, P, f/.1, f/.len f by A1,A4,Th24;
LE q, f/.(j+1), P, f/.1, f/.len f by A1,Th26;
then A6: LE q, p1, P, f/.1, f/.len f by A3,A5,Th13;
LE p1, q1, P, f/.1, f/.len f by A1,Th25;
then A7: LE q, q1, P, f/.1, f/.len f by A3,A6,Th13;
P is closed by SPPOL_1:49;
then A8: L~f meets Q & L~f /\ Q is closed &
P is_an_arc_of f/.1, f/.len f
by A1,TOPREAL1:31,TOPS_1:35;
then LE q1, q, P, f/.1, f/.len f by A1,A2,Th15;
hence contradiction by A1,A7,A8,Th12;
end;
assume i = j;
hence thesis by A1,Lm3;
end;
theorem
for f being FinSequence of TOP-REAL 2,
Q being Subset of TOP-REAL 2,
q being Point of TOP-REAL 2,
i, j being Nat st
L~f meets Q & f is_S-Seq & Q is closed &
Last_Point (L~f,f/.1,f/.len f,Q) in LSeg(f,i) & 1<=i & i+1<=len f &
q in LSeg(f,j) & 1 <= j & j + 1 <= len f & q in Q &
Last_Point (L~f,f/.1,f/.len f,Q) <> q holds
i >= j &
(i=j implies LE q, Last_Point(L~f,f/.1,f/.len f,Q), f/.i, f/.(i+1))
proof
let f be FinSequence of TOP-REAL 2,
Q be Subset of TOP-REAL 2,
q be Point of TOP-REAL 2, i,j be Nat;
assume A1: L~f meets Q & f is_S-Seq & Q is closed
& Last_Point(L~f,f/.1,f/.len f,Q) in LSeg(f,i) & 1<=i & i+1<=len f
& q in LSeg(f,j) & 1<=j & j+1<=len f & q in Q
& Last_Point (L~f,f/.1,f/.len f,Q) <> q;
then A2: q in L~f by SPPOL_2:17;
reconsider P = L~f as non empty Subset of TOP-REAL 2 by A1,
SPPOL_2:17;
set q1 = Last_Point(P,f/.1,f/.len f,Q), p2 = f/.(i+1);
A3: P is_an_arc_of f/.1, f/.len f by A1,TOPREAL1:31;
thus i >= j
proof
assume j > i;
then A4: i+1 <= j by NAT_1:38;
i <= i + 1 & j <= j + 1 by NAT_1:29;
then 1 <= i + 1 & j <= len f by A1,AXIOMS:22;
then A5:LE p2, f/.j, P, f/.1, f/.len f by A1,A4,Th24;
LE f/.j, q, P, f/.1, f/.len f by A1,Th25;
then A6:LE p2, q, P, f/.1, f/.len f by A3,A5,Th13;
LE q1, p2, P, f/.1, f/.len f by A1,Th26;
then A7:LE q1, q, P, f/.1, f/.len f by A3,A6,Th13;
L~f is closed by SPPOL_1:49;
then A8: L~f meets Q & L~f /\ Q is closed &
P is_an_arc_of f/.1, f/.len f by A1,TOPREAL1:31,TOPS_1:35;
then LE q, q1, P, f/.1, f/.len f by A1,A2,Th16;
hence contradiction by A1,A7,A8,Th12;
end;
assume i = j;
hence thesis by A1,Lm5;
end;
theorem Th29:
for f being FinSequence of TOP-REAL 2,
q1, q2 being Point of TOP-REAL 2,
i being Nat st
q1 in LSeg(f,i) & q2 in LSeg(f,i) & f is_S-Seq & 1 <= i & i + 1 <= len f
holds LE q1, q2, L~f, f/.1, f/.len f implies
LE q1, q2, LSeg (f,i), f/.i, f/.(i+1)
proof
let f be FinSequence of TOP-REAL 2,
q1, q2 be Point of TOP-REAL 2,
i be Nat;
assume
A1: q1 in LSeg(f,i) & q2 in LSeg(f,i) & f is_S-Seq & 1 <= i & i + 1 <=
len f;
then A2: L~f is_an_arc_of f/.1, f/.len f by TOPREAL1:31;
assume A3: LE q1, q2, L~f, f/.1, f/.len f;
len f >= 2 by A1,TOPREAL1:def 10;
then reconsider P = L~f, Q = LSeg(f,i) as non empty Subset of
TOP-REAL 2 by A1,TOPREAL1:29;
consider F being map of I[01], (TOP-REAL 2)|P such that
A4: F is_homeomorphism & F.0 = f/.1 & F.1 = f/.len f
by A2,TOPREAL1:def 2;
consider ppi, pi1 be Real such that
A5: ppi < pi1 & 0 <= ppi & ppi <= 1 & 0 <= pi1 & pi1 <= 1 &
LSeg (f, i) = F.:[.ppi, pi1.] & F.ppi = f/.i & F.pi1 = f/.(i+1)
by A1,A4,JORDAN5B:7;
A6: ppi in { dd where dd is Real : ppi <= dd & dd <= pi1 } &
pi1 in { dd where dd is Real : ppi <= dd & dd <= pi1 } by A5;
then A7: ppi in [.ppi,pi1.] & pi1 in [.ppi,pi1.] by RCOMP_1:def 1;
[.ppi,pi1.] c= [.0,1.] by A5,TREAL_1:1;
then reconsider Poz = [.ppi,pi1.] as non empty Subset of I[01]
by A6,BORSUK_1:83,RCOMP_1:def 1;
consider G be map of I[01]|Poz, (TOP-REAL 2)|Q such that
A8: G = F|Poz & G is_homeomorphism by A1,A4,A5,JORDAN5B:8;
set Ex = L[01]((#)(ppi,pi1),(ppi,pi1)(#));
set H = G * Ex;
A9: Ex is_homeomorphism by A5,TREAL_1:20;
then A10: rng Ex = [#] Closed-Interval-TSpace(ppi,pi1) by TOPS_2:def 5;
then A11: rng Ex = the carrier of Closed-Interval-TSpace(ppi,pi1) by
PRE_TOPC:12;
A12: dom G = [#](I[01]|Poz) by A8,TOPS_2:def 5
.= Poz by PRE_TOPC:def 10
.= the carrier of Closed-Interval-TSpace(ppi,pi1) by A5,TOPMETR:25
.= [#] Closed-Interval-TSpace(ppi,pi1) by PRE_TOPC:12;
then A13: dom H = dom Ex by A10,RELAT_1:46
.= [#] I[01] by A9,TOPMETR:27,TOPS_2:def 5
.= the carrier of I[01] by PRE_TOPC:12;
A14: rng H = rng G by A10,A12,RELAT_1:47
.= [#] ((TOP-REAL 2)|LSeg(f,i)) by A8,TOPS_2:def 5;
then H is Function of the carrier of I[01],
the carrier of (TOP-REAL 2)|Q
by A13,FUNCT_2:4;
then reconsider H as map of I[01], (TOP-REAL 2)|Q;
reconsider K1 = Closed-Interval-TSpace(ppi,pi1),
K2 = I[01]|Poz as SubSpace of I[01]
by A5,TOPMETR:27,TREAL_1:6;
the carrier of K1 = [.ppi,pi1.] by A5,TOPMETR:25
.= [#](I[01]|Poz) by PRE_TOPC:def 10
.= the carrier of K2 by PRE_TOPC:12;
then I[01] = Closed-Interval-TSpace(0,1) &
I[01]|Poz = Closed-Interval-TSpace(ppi,pi1) by TOPMETR:27,TSEP_1:5;
then A15: H is_homeomorphism by A8,A9,TOPS_2:71;
A16: Ex.0 = Ex.(#)(0,1) by TREAL_1:def 1
.= (#)(ppi,pi1) by A5,TREAL_1:12
.= ppi by A5,TREAL_1:def 1;
0 in dom H by A13,JORDAN5A:2;
then A17: H.0 = G.ppi by A16,FUNCT_1:22
.= f/.i by A5,A7,A8,FUNCT_1:72;
A18: Ex.1 = Ex.(0,1)(#) by TREAL_1:def 2
.= (ppi,pi1)(#) by A5,TREAL_1:12
.= pi1 by A5,TREAL_1:def 2;
1 in dom H by A13,JORDAN5A:2;
then A19: H.1 = G.pi1 by A18,FUNCT_1:22
.= f/.(i+1) by A5,A7,A8,FUNCT_1:72;
A20: Q is_an_arc_of f/.i, f/.(i+1) by A1,JORDAN5B:15;
q1 in rng H by A1,A14,PRE_TOPC:def 10;
then consider x1' be set such that
A21: x1' in dom H & q1 = H.x1' by FUNCT_1:def 5;
q2 in rng H by A1,A14,PRE_TOPC:def 10;
then consider x2' be set such that
A22: x2' in dom H & q2 = H.x2' by FUNCT_1:def 5;
A23: x1' in { l where l is Real : 0 <= l & l <= 1 } &
x2' in { l where l is Real : 0 <= l & l <= 1 }
by A13,A21,A22,BORSUK_1:83,RCOMP_1:def 1;
then consider x1 be Real such that
A24: x1 = x1' & 0 <= x1 & x1 <= 1;
consider x2 be Real such that
A25: x2 = x2' & 0 <= x2 & x2 <= 1 by A23;
A26: x1 in the carrier of I[01] & x2 in the carrier of I[01]
by A24,A25,JORDAN5A:2;
reconsider X1 = x1, X2 = x2 as Point of Closed-Interval-TSpace (0,1)
by A24,A25,JORDAN5A:2,TOPMETR:27;
x1 in dom Ex & x2 in dom Ex by A10,A12,A13,A26,RELAT_1:46;
then Ex.x1 in the carrier of Closed-Interval-TSpace(ppi,pi1) &
Ex.x2 in the carrier of Closed-Interval-TSpace(ppi,pi1)
by A11,FUNCT_1:def 5;
then A27: Ex.x1 in Poz & Ex.x2 in Poz by A5,TOPMETR:25;
A28: q1 = G.(Ex.x1) by A21,A24,FUNCT_1:22
.= F.(Ex.x1) by A8,A27,FUNCT_1:72;
A29: q2 = G.(Ex.x2) by A22,A25,FUNCT_1:22
.= F.(Ex.x2) by A8,A27,FUNCT_1:72;
reconsider E1 = Ex.X1, E2 = Ex.X2 as Real by A27;
0 <= E1 & E1 <= 1 & 0 <= E2 & E2 <= 1 by A27,JORDAN5A:2;
then A30: E1 <= E2 by A3,A4,A28,A29,Def3;
Ex is one-to-one continuous by A9,TOPS_2:def 5;
then x1 <= x2 by A5,A16,A18,A30,JORDAN5A:16;
hence thesis by A15,A17,A19,A20,A21,A22,A24,A25,Th8;
end;
theorem
for f being FinSequence of TOP-REAL 2,
q1, q2 being Point of TOP-REAL 2 st
q1 in L~f & q2 in L~f & f is_S-Seq & q1 <> q2
holds LE q1, q2, L~f, f/.1, f/.len f iff
for i, j being Nat st q1 in LSeg(f,i) & q2 in LSeg(f,j)
& 1 <= i & i+1 <= len f
& 1 <= j & j+1 <= len f holds
i <= j & (i = j implies LE q1,q2,f/.i,f/.(i+1))
proof
let f be FinSequence of TOP-REAL 2,
q1,q2 be Point of TOP-REAL 2;
set p3 = f/.1, p4 = f/.len f;
assume A1: q1 in L~f & q2 in L~f & f is_S-Seq & q1 <> q2;
then A2: L~f is_an_arc_of p3, p4 by TOPREAL1:31;
reconsider P = L~f as non empty Subset of TOP-REAL 2 by A1;
hereby assume A3: LE q1,q2,L~f,f/.1,f/.len f;
thus for i,j being Nat st q1 in LSeg(f,i) & q2 in LSeg(f,j)
& 1<=i & i+1<=len f
& 1<=j & j+1<=len f holds i<=j & (i=j implies LE q1,q2,f/.i,f/.(i+1))
proof
let i,j be Nat;
assume
A4:q1 in LSeg(f,i) & q2 in LSeg(f,j) & 1<=i & i+1<=len f & 1<=j & j+1<=len f;
thus i<=j
proof
assume j < i;
then j+1 <= i by NAT_1:38;
then consider m be Nat such that
A5: j+1+m = i by NAT_1:28;
A6: LE q2, f/.(j+1), P, p3, p4 by A1,A4,Th26;
i <= i + 1 & j <= j + 1 by NAT_1:29;
then 1 <= j+1 & j+1 <= j+1+m & j+1+m <= len f
by A4,A5,AXIOMS:22,NAT_1:29;
then LE f/.(j+1), f/.(j+1+m), P, p3, p4 by A1,Th24;
then A7: LE q2, f/.(j+1+m), P, p3, p4 by A2,A6,Th13;
LE f/.(j+1+m), q1, P, p3, p4 by A1,A4,A5,Th25;
then LE q2, q1, P, p3, p4 by A2,A7,Th13;
hence thesis by A1,A2,A3,Th12;
end;
assume A8: i = j;
set p1 = f/.i, p2 = f/.(i+1);
A9:i in dom f & i+1 in dom f by A4,GOBOARD2:3;
A10:LSeg (f,i) = LSeg (p1, p2) by A4,TOPREAL1:def 5;
reconsider Q = LSeg (f,i) as non empty Subset of TOP-REAL 2
by A4;
A11:f is one-to-one by A1,TOPREAL1:def 10;
A12:p1 <> p2
proof
assume p1 = p2;
then i = i+1 by A9,A11,PARTFUN2:17;
hence thesis by REAL_1:69;
end;
LE q1, q2, Q, p1, p2 by A1,A3,A4,A8,Th29;
hence LE q1,q2,p1,p2 by A10,A12,Th17;
end;
end;
assume A13: for i,j being Nat st q1 in LSeg(f,i) & q2 in LSeg(f,j)
& 1<=i & i+1<=len f
& 1<=j & j+1<=len f holds i<=j & (i=j implies LE q1,q2,f/.i,f/.(i+1));
consider i be Nat such that
A14: 1 <= i & i+1 <= len f & q1 in LSeg(f,i) by A1,SPPOL_2:13;
consider j be Nat such that
A15: 1 <= j & j+1 <= len f & q2 in LSeg(f,j) by A1,SPPOL_2:13;
A16: i<=j & (i=j implies LE q1,q2,f/.i,f/.(i+1)) by A13,A14,A15;
A17: P is_an_arc_of f/.1, f/.len f by A1,TOPREAL1:31;
per cases by A16,REAL_1:def 5;
suppose i < j;
then i+1 <= j by NAT_1:38;
then consider m be Nat such that
A18: j = i+1 + m by NAT_1:28;
A19: 1 <= i+1 & i+1+m+1 <= len f by A15,A18,NAT_1:37;
A20: LE q1, f/.(i+1), P, f/.1, f/.len f by A1,A14,Th26;
i <= i + 1 & j <= j + 1 by NAT_1:29;
then i+1 <= i+1+m & i+1+m <= len f by A15,A18,AXIOMS:22,NAT_1:29;
then LE f/.(i+1), f/.(i+1+m), P, f/.1, f/.len f by A1,A19,Th24;
then A21: LE q1, f/.(i+1+m), P, f/.1, f/.len f by A17,A20,Th13;
LE f/.(i+1+m), q2, P, f/.1, f/.len f by A1,A15,A18,Th25;
hence LE q1, q2, L~f, f/.1, f/.len f by A17,A21,Th13;
suppose A22: i = j;
then A23: LE q1, q2, f/.i, f/.(i+1) by A13,A14,A15;
set p1 = f/.i,p2 = f/.(i+1);
A24:i in dom f & i+1 in dom f by A14,GOBOARD2:3;
A25:f is one-to-one by A1,TOPREAL1:def 10;
p1 <> p2
proof
assume p1 = p2;
then i = i+1 by A24,A25,PARTFUN2:17;
hence thesis by REAL_1:69;
end;
then consider H be map of I[01], (TOP-REAL 2) | LSeg(p1, p2) such that
A26: (for x being Real st x in [.0,1.] holds H.x = (1-x)*p1 + x*p2) &
H is_homeomorphism & H.0 = p1 & H.1 = p2 by JORDAN5A:4;
A27: LSeg(f,i) = LSeg(p1,p2) by A14,TOPREAL1:def 5;
reconsider Q = LSeg (f,i) as non empty Subset of TOP-REAL 2 by A14;
reconsider H as map of I[01], (TOP-REAL 2) | Q by A27;
q1 in P & q2 in P &
for g being map of I[01], (TOP-REAL 2)|P, s1,s2 be Real st
g is_homeomorphism
& g.0=f/.1 & g.1=f/.len f
& g.s1=q1 & 0<=s1 & s1<=1
& g.s2=q2 & 0<=s2 & s2<=1
holds s1<=s2
proof
thus q1 in P & q2 in P by A1;
let F be map of I[01], (TOP-REAL 2)|P, s1, s2 be Real;
assume A28: F is_homeomorphism
& F.0 = f/.1 & F.1 = f/.len f
& F.s1 = q1 & 0 <= s1 & s1 <= 1 & F.s2 = q2 & 0 <= s2 & s2 <= 1;
then A29: s1 in the carrier of I[01] & s2 in the carrier of I[01] by JORDAN5A:2
;
A30: dom F = [#] I[01] by A28,TOPS_2:def 5
.= the carrier of I[01] by PRE_TOPC:12;
A31: F is one-to-one by A28,TOPS_2:def 5;
consider ppi, pi1 be Real such that
A32: ppi < pi1 & 0 <= ppi & ppi <= 1 & 0 <= pi1 & pi1 <= 1 &
LSeg (f, i) = F.:[.ppi, pi1.] & F.ppi = f/.i & F.pi1 = f/.(i+1)
by A1,A14,A28,JORDAN5B:7;
A33: ppi in { dd where dd is Real : ppi <= dd & dd <= pi1 } &
pi1 in { dd where dd is Real : ppi <= dd & dd <= pi1 } by A32;
then A34: ppi in [.ppi,pi1.] & pi1 in [.ppi,pi1.] by RCOMP_1:def 1;
[.ppi,pi1.] c= [.0,1.] by A32,TREAL_1:1;
then reconsider Poz = [.ppi,pi1.] as non empty Subset of I[01]
by A33,BORSUK_1:83,RCOMP_1:def 1;
consider G be map of I[01]|Poz, (TOP-REAL 2)|Q such that
A35: G = F|Poz & G is_homeomorphism by A1,A14,A28,A32,JORDAN5B:8;
A36:dom H = [#]I[01] by A26,TOPS_2:def 5
.= [.0,1.] by BORSUK_1:83,PRE_TOPC:12;
A37:rng H = [#] ((TOP-REAL 2) | LSeg(f,i)) by A26,A27,TOPS_2:def 5
.= LSeg (f,i) by PRE_TOPC:def 10;
then consider x1' be set such that
A38: x1' in dom H & H.x1' = q1 by A14,FUNCT_1:def 5;
x1' in { l where l is Real : 0 <= l & l <= 1 }
by A36,A38,RCOMP_1:def 1;
then consider x1 be Real such that
A39: x1 = x1' & 0 <= x1 & x1 <= 1;
consider x2' be set such that
A40: x2' in dom H & H.x2' = q2 by A15,A22,A37,FUNCT_1:def 5;
x2' in { l where l is Real : 0 <= l & l <= 1 }
by A36,A40,RCOMP_1:def 1;
then consider x2 be Real such that
A41: x2 = x2' & 0 <= x2 & x2 <= 1;
reconsider K1 = Closed-Interval-TSpace(ppi,pi1),
K2 = I[01]|Poz as SubSpace of I[01]
by A32,TOPMETR:27,TREAL_1:6;
A42: the carrier of K1 = [.ppi,pi1.] by A32,TOPMETR:25
.= [#](I[01]|Poz) by PRE_TOPC:def 10
.= the carrier of K2 by PRE_TOPC:12;
then A43:Closed-Interval-TSpace(ppi,pi1) = I[01]|Poz by TSEP_1:5;
reconsider E=G" * H as map of Closed-Interval-TSpace(0,1),
Closed-Interval-TSpace(ppi,pi1)
by A42,TOPMETR:27;
G" is_homeomorphism & H is_homeomorphism by A26,A27,A35,TOPS_2:70;
then E is_homeomorphism by A43,TOPMETR:27,TOPS_2:71;
then A44:E is continuous one-to-one by TOPS_2:def 5;
A45:dom G = [#] (I[01]|Poz) & rng G = [#] ((TOP-REAL 2)|LSeg(f,i)) &
G is one-to-one by A35,TOPS_2:def 5;
then A46:dom G = Poz by PRE_TOPC:def 10;
A47:G" = (G qua Function)" by A45,TOPS_2:def 4;
0 in { l where l is Real : 0 <= l & l <= 1 } &
1 in { l where l is Real : 0 <= l & l <= 1 };
then A48:0 in [.0,1.] & 1 in [.0,1.] by RCOMP_1:def 1;
then A49:H.0 = (1-0)*p1 + 0 * p2 by A26
.= p1 + 0 * p2 by EUCLID:33
.= p1 + 0.REAL 2 by EUCLID:33
.= p1 by EUCLID:31;
A50:H.1 = (1-1)*p1 + 1*p2 by A26,A48
.= 0.REAL 2 + 1*p2 by EUCLID:33
.= 0.REAL 2 + p2 by EUCLID:33
.= p2 by EUCLID:31;
G.ppi = p1 by A32,A34,A35,FUNCT_1:72;
then A51:ppi = G".(H.0) by A34,A45,A46,A47,A49,FUNCT_1:54
.= E.0 by A36,A48,FUNCT_1:23;
G.pi1 = p2 by A32,A34,A35,FUNCT_1:72;
then A52:pi1 = G".(H.1) by A34,A45,A46,A47,A50,FUNCT_1:54
.= E.1 by A36,A48,FUNCT_1:23;
consider x be set such that
A53: x in dom F & x in [.ppi,pi1.] & q1 = F.x by A14,A32,FUNCT_1:def 12;
A54:x = s1 by A28,A29,A30,A31,A53,FUNCT_1:def 8;
A55:s1 in dom G by A28,A29,A30,A31,A46,A53,FUNCT_1:def 8;
G.s1 = q1 by A35,A53,A54,FUNCT_1:72;
then A56:s1 = G".(H.x1) by A38,A39,A45,A47,A55,FUNCT_1:54
.= E.x1 by A38,A39,FUNCT_1:23;
consider x' be set such that
A57: x' in dom F & x' in [.ppi,pi1.] & q2 = F.x'
by A15,A22,A32,FUNCT_1:def 12;
A58:s2 in Poz by A28,A29,A30,A31,A57,FUNCT_1:def 8;
A59:s2 in dom G by A28,A29,A30,A31,A46,A57,FUNCT_1:def 8;
G.s2 = q2 by A28,A35,A58,FUNCT_1:72;
then A60:s2 = G".(H.x2) by A40,A41,A45,A47,A59,FUNCT_1:54
.= E.x2 by A40,A41,FUNCT_1:23;
reconsider X1 = x1, X2 = x2 as Point of Closed-Interval-TSpace(0,1)
by A36,A38,A39,A40,A41,TOPMETR:25;
A61:s1 = E.X1 & s2 = E.X2 by A56,A60;
A62:q1 = (1-x1)*p1 + x1*p2 by A26,A36,A38,A39;
q2 = (1-x2)*p1 + x2*p2 by A26,A36,A40,A41;
then A63:x1 <= x2 by A23,A39,A41,A62,JORDAN3:def 6;
per cases by A63,REAL_1:def 5;
suppose x1 = x2;
hence thesis by A56,A60;
suppose x1 < x2;
hence thesis by A32,A44,A51,A52,A61,JORDAN5A:16;
end;
hence LE q1, q2, L~f, f/.1, f/.len f by Def3;
end;