:: The Ordering of Points on a Curve, Part { II }
:: by Adam Grabowski and Yatsuka Nakamura
::
:: Received September 10, 1997
:: Copyright (c) 1997-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, SUBSET_1, EUCLID, PRE_TOPC, FUNCT_1, BORSUK_1, RELAT_1,
REAL_1, TOPS_2, CARD_1, XXREAL_0, ARYTM_3, XBOOLE_0, ORDINAL2, STRUCT_0,
RCOMP_1, TOPREAL1, TARSKI, JORDAN3, XXREAL_1, FINSEQ_1, PARTFUN1,
RLTOPSP1, ARYTM_1, TREAL_1, VALUED_1, TOPMETR, NAT_1, SUPINF_2, JORDAN5C,
FUNCT_2;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, REAL_1, XCMPLX_0,
XREAL_0, NAT_1, RCOMP_1, RELAT_1, FINSEQ_1, FUNCT_1, RELSET_1, PARTFUN1,
FUNCT_2, TOPMETR, JORDAN3, STRUCT_0, TOPREAL1, PRE_TOPC, TOPS_2,
COMPTS_1, RLVECT_1, RLTOPSP1, EUCLID, TREAL_1, XXREAL_0;
constructors REAL_1, RCOMP_1, TOPS_2, COMPTS_1, TOPREAL1, TREAL_1, JORDAN3;
registrations FUNCT_1, RELSET_1, FUNCT_2, MEMBERED, STRUCT_0, PRE_TOPC,
BORSUK_1, EUCLID, TOPREAL1, SPPOL_1, XREAL_0, NAT_1, ORDINAL1;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
definitions TARSKI, JORDAN3, XBOOLE_0;
equalities XBOOLE_0, STRUCT_0;
expansions JORDAN3, XBOOLE_0;
theorems BORSUK_1, COMPTS_1, FUNCT_1, FUNCT_2, RELAT_1, GOBOARD1, NAT_1,
GOBOARD9, TOPS_1, PRE_TOPC, RCOMP_1, HEINE, PCOMPS_1, SPPOL_2, TARSKI,
TOPMETR, TOPREAL1, TOPREAL3, TSEP_1, JORDAN5B, TOPS_2, TREAL_1, JORDAN5A,
ZFMISC_1, PARTFUN2, XBOOLE_0, XBOOLE_1, FINSEQ_3, XXREAL_0, XXREAL_1,
XREAL_1, SEQ_4, RELSET_1, RLVECT_1;
schemes NAT_1;
begin :: First and last point of a curve
theorem Th1:
for P, Q being Subset of TOP-REAL 2, p1, p2, q1 being Point of
TOP-REAL 2, f being Function of I[01], (TOP-REAL 2)|P,
s1 be Real st q1 in P &
f.s1 = q1 & f is being_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)
for g being Function of I[01], (TOP-REAL 2)|P, s2 be Real
st g is being_homeomorphism & g.0
= p1 & g.1 = p2 & g.s2 = q1 & 0 <= s2 & s2 <= 1
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
Function of I[01], (TOP-REAL 2)|P, s1 be Real;
assume that
A1: q1 in P and
A2: f.s1=q1 and
A3: f is being_homeomorphism and
A4: f.0=p1 and
A5: f.1=p2 and
A6: 0 <= s1 & s1 <= 1 and
A7: for t being Real st 0<=t & t<s1 holds not f.t in Q;
reconsider P9=P as non empty Subset of TOP-REAL 2 by A1;
let g be Function of I[01], (TOP-REAL 2)|P, s2 be Real;
assume that
A8: g is being_homeomorphism and
A9: g.0=p1 and
A10: g.1=p2 and
A11: g.s2=q1 and
A12: 0<=s2 and
A13: s2<=1;
reconsider f,g as Function of I[01], (TOP-REAL 2)|P9;
A14: f is one-to-one by A3,TOPS_2:def 5;
A15: dom f = [#]I[01] by A3,TOPS_2:def 5;
then
A16: 1 in dom f by BORSUK_1:43;
A17: rng f = [#]((TOP-REAL 2)|P) by A3,TOPS_2:def 5;
then f is onto by FUNCT_2:def 3;
then
A18: f" = (f qua Function)" by A14,TOPS_2:def 4;
A19: f".p2 = 1 by A5,A16,A14,A18,FUNCT_1:32;
A20: 0 in dom f by A15,BORSUK_1:43;
A21: f".p1 = 0 by A4,A20,A14,A18,FUNCT_1:32;
set fg = f"*g;
A22: f" is being_homeomorphism by A3,TOPS_2:56;
then fg is being_homeomorphism by A8,TOPS_2:57;
then
A23: fg is continuous & fg is one-to-one by TOPS_2:def 5;
let t be Real;
assume that
A24: 0<=t and
A25: t<s2;
A26: t <= 1 by A13,A25,XXREAL_0:2;
then reconsider t1 = t, s29 = s2 as Point of I[01] by A12,A13,A24,BORSUK_1:43
;
A27: t in the carrier of I[01] by A24,A26,BORSUK_1:43;
reconsider Ft = fg.t1 as Real by BORSUK_1:40;
A28: rng g = [#]((TOP-REAL 2)|P) by A8,TOPS_2:def 5;
A29: dom g = [#]I[01] by A8,TOPS_2:def 5;
then 1 in dom g by BORSUK_1:43;
then
A30: (f"*g).1 = 1 by A10,A19,FUNCT_1:13;
A31: s1 in dom f by A6,A15,BORSUK_1:43;
dom (f") = [#]((TOP-REAL 2)|P) by A22,TOPS_2:def 5;
then
A32: dom (f"*g) = dom g by A28,RELAT_1:27;
0 in dom g by A29,BORSUK_1:43;
then
A33: (f"*g).0 = 0 by A9,A21,FUNCT_1:13;
A34: 0 <= Ft
proof
per cases by A24;
suppose
0<t;
hence thesis by A23,A33,A30,BORSUK_1:def 14,JORDAN5A:15,TOPMETR:20;
end;
suppose
0 = t;
hence thesis by A9,A21,A29,FUNCT_1:13;
end;
end;
f*(f"*g) = (g qua Relation) * (f * f") by RELAT_1:36
.= (g qua Relation) * id rng f by A17,A14,TOPS_2:52
.= id rng g * g by A8,A17,TOPS_2:def 5
.= g by RELAT_1:54;
then
A35: f.((f"*g).t) = g.t by A29,A27,A32,FUNCT_1:13;
s2 in dom g by A12,A13,A29,BORSUK_1:43;
then (f"*g).s2 = f".q1 by A11,FUNCT_1:13
.= s1 by A2,A14,A31,A18,FUNCT_1:32;
then fg.s29 = s1;
then Ft < s1 by A25,A23,A33,A30,JORDAN5A:15,TOPMETR:20;
hence thesis by A7,A34,A35;
end;
definition
let P, Q be Subset of TOP-REAL 2, p1, p2 be Point of TOP-REAL 2;
assume that
A1: P meets Q & P /\ Q is closed and
A2: 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 Function of I[01], (TOP-REAL 2)|P, s2 being Real
st g is
being_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
A3: EX in P /\ Q and
A4: ex g being Function of I[01], (TOP-REAL 2)|P, s2 be Real st g is
being_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,A2,JORDAN5A:21;
EX in P by A3,XBOOLE_0:def 4;
then for g being Function of I[01], (TOP-REAL 2)|P,
s2 be Real st g is
being_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 A4,Th1;
hence thesis by A3;
end;
uniqueness
proof
let IT1, IT2 be Point of TOP-REAL 2;
A5: P /\ Q c= Q by XBOOLE_1:17;
A6: P /\ Q c= P by XBOOLE_1:17;
assume that
A7: IT1 in P /\ Q and
A8: for g1 being Function of I[01], (TOP-REAL 2)|P, s1 be Real st g1
is being_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 that
A9: IT2 in P /\ Q and
A10: for g2 being Function of I[01], (TOP-REAL 2)|P, s2 be Real st g2
is being_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 Function of I[01], (TOP-REAL 2)|P such that
A11: g is being_homeomorphism and
A12: g.0=p1 & g.1=p2 by A2,TOPREAL1:def 1;
A13: rng g = [#]((TOP-REAL 2)|P) by A11,TOPS_2:def 5
.= P by PRE_TOPC:def 5;
then consider ss1 be object such that
A14: ss1 in dom g and
A15: g.ss1 = IT1 by A6,A7,FUNCT_1:def 3;
reconsider ss1 as Real by A14,BORSUK_1:40;
A16: 0 <= ss1 by A14,BORSUK_1:43;
consider ss2 be object such that
A17: ss2 in dom g and
A18: g.ss2 = IT2 by A6,A9,A13,FUNCT_1:def 3;
reconsider ss2 as Real by A17,BORSUK_1:40;
A19: 0 <= ss2 by A17,BORSUK_1:43;
A20: ss1 <= 1 by A14,BORSUK_1:43;
A21: ss2 <= 1 by A17,BORSUK_1:43;
per cases by XXREAL_0:1;
suppose
ss1 < ss2;
hence thesis by A5,A7,A10,A11,A12,A15,A18,A16,A21;
end;
suppose
ss1 = ss2;
hence thesis by A15,A18;
end;
suppose
ss1 > ss2;
hence thesis by A5,A8,A9,A11,A12,A15,A18,A20,A19;
end;
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;
assume that
A1: p in P and
A2: P is_an_arc_of p1, p2 and
A3: Q = {p};
A4: P /\ {p} = {p} by A1,ZFMISC_1:46;
A5: for g being Function of I[01], (TOP-REAL 2)|P, s2 be Real st g is
being_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 Function of I[01], (TOP-REAL 2)|P, s2 be Real;
assume that
A6: g is being_homeomorphism and
g.0=p1 and
g.1=p2 and
A7: g.s2=p and
A8: 0<=s2 and
A9: s2<=1;
A10: g is one-to-one by A6,TOPS_2:def 5;
let t be Real;
assume that
A11: 0<=t and
A12: t<s2;
A13: dom g = the carrier of I[01] by A1,FUNCT_2:def 1;
t <= 1 by A9,A12,XXREAL_0:2;
then
A14: t in dom g by A13,A11,BORSUK_1:43;
s2 in dom g by A8,A9,A13,BORSUK_1:43;
then g.t <> g.s2 by A10,A12,A14,FUNCT_1:def 4;
hence thesis by A7,TARSKI:def 1;
end;
A15: P /\ Q is closed by A3,A4,PCOMPS_1:7;
A16: p in P /\ {p} by A4,TARSKI:def 1;
then P meets {p};
hence thesis by A2,A3,A16,A15,A5,Def1;
end;
theorem Th3:
for P, 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, Q be Subset of TOP-REAL 2, p1,p2 be Point of TOP-REAL 2;
assume that
A1: p1 in Q and
A2: P /\ Q is closed and
A3: P is_an_arc_of p1, p2;
A4: for g being Function of I[01], (TOP-REAL 2)|P, s2 be Real st g is
being_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 Function of I[01], (TOP-REAL 2)|P, s2 be Real;
assume that
A5: g is being_homeomorphism and
A6: g.0=p1 and
g.1=p2 and
A7: g.s2=p1 and
A8: 0<=s2 & s2<=1;
A9: g is one-to-one by A5,TOPS_2:def 5;
let t be Real;
assume
A10: 0<=t & t<s2;
A11: dom g = [#] I[01] by A5,TOPS_2:def 5
.= the carrier of I[01];
then
A12: 0 in dom g by BORSUK_1:43;
s2 in dom g by A8,A11,BORSUK_1:43;
hence thesis by A6,A7,A12,A9,A10,FUNCT_1:def 4;
end;
p1 in P by A3,TOPREAL1:1;
then p1 in P /\ Q & P meets Q by A1,XBOOLE_0:def 4;
hence thesis by A2,A3,A4,Def1;
end;
theorem Th4:
for P, Q being Subset of TOP-REAL 2, p1, p2, q1 being Point of
TOP-REAL 2, f being Function of I[01], (TOP-REAL 2)|P, s1 be Real
st q1 in P &
f.s1 = q1 & f is being_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)
for g being
Function of I[01], (TOP-REAL 2)|P, s2 being Real
st g is being_homeomorphism &
g.0 = p1 & g.1 = p2 & g.s2 = q1 & 0 <= s2 & s2 <= 1
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
Function of I[01], (TOP-REAL 2)|P, s1 be Real;
assume that
A1: q1 in P and
A2: f.s1=q1 and
A3: f is being_homeomorphism and
A4: f.0=p1 and
A5: f.1=p2 and
A6: 0 <= s1 & s1 <= 1 and
A7: for t being Real st 1>=t & t>s1 holds not f.t in Q;
reconsider P9=P as non empty Subset of TOP-REAL 2 by A1;
let g be Function of I[01], (TOP-REAL 2)|P, s2 be Real;
assume that
A8: g is being_homeomorphism and
A9: g.0=p1 and
A10: g.1=p2 and
A11: g.s2=q1 and
A12: 0<=s2 and
A13: s2<=1;
reconsider f, g as Function of I[01], (TOP-REAL 2)|P9;
A14: f is one-to-one by A3,TOPS_2:def 5;
set fg = f"*g;
let t be Real;
assume that
A15: 1>=t and
A16: t>s2;
reconsider t1 = t, s29 = s2 as Point of I[01] by A12,A13,A15,A16,BORSUK_1:43;
A17: t in the carrier of I[01] by A12,A15,A16,BORSUK_1:43;
reconsider Ft = fg.t1 as Real by BORSUK_1:40;
A18: rng g = [#]((TOP-REAL 2)|P) by A8,TOPS_2:def 5;
A19: f" is being_homeomorphism by A3,TOPS_2:56;
then fg is being_homeomorphism by A8,TOPS_2:57;
then
A20: fg is continuous & fg is one-to-one by TOPS_2:def 5;
A21: dom f = [#]I[01] by A3,TOPS_2:def 5;
then
A22: 0 in dom f by BORSUK_1:43;
A23: rng f = [#]((TOP-REAL 2)|P) by A3,TOPS_2:def 5;
then f is onto by FUNCT_2:def 3;
then
A24: f" = (f qua Function)" by A14,TOPS_2:def 4;
then
A25: f".p1 = 0 by A4,A22,A14,FUNCT_1:32;
A26: 1 in dom f by A21,BORSUK_1:43;
A27: f".p2 = 1 by A24,A5,A26,A14,FUNCT_1:32;
A28: dom g = [#]I[01] by A8,TOPS_2:def 5;
then 0 in dom g by BORSUK_1:43;
then
A29: (f"*g).0 = 0 by A9,A25,FUNCT_1:13;
1 in dom g by A28,BORSUK_1:43;
then
A30: (f"*g).1 = 1 by A10,A27,FUNCT_1:13;
A31: Ft <= 1
proof
per cases by A15,XXREAL_0:1;
suppose
t<1;
hence thesis by A20,A29,A30,BORSUK_1:def 15,JORDAN5A:15,TOPMETR:20;
end;
suppose
t=1;
hence thesis by A10,A27,A28,FUNCT_1:13;
end;
end;
dom (f") = [#]((TOP-REAL 2)|P) by A19,TOPS_2:def 5;
then
A32: t in dom (f"*g) by A28,A18,A17,RELAT_1:27;
f*(f"*g) = (g qua Relation) * (f * f") by RELAT_1:36
.= (g qua Relation) * id rng f by A23,A14,TOPS_2:52
.= id rng g * g by A8,A23,TOPS_2:def 5
.= g by RELAT_1:54;
then
A33: f.((f"*g).t) = g.t by A32,FUNCT_1:13;
A34: s1 in dom f by A6,A21,BORSUK_1:43;
s2 in dom g by A12,A13,A28,BORSUK_1:43;
then (f"*g).s2 = f".q1 by A11,FUNCT_1:13
.= s1 by A2,A14,A34,A24,FUNCT_1:32;
then fg.s29 = s1;
then s1 < Ft by A16,A20,A29,A30,JORDAN5A:15,TOPMETR:20;
hence thesis by A7,A31,A33;
end;
definition
let P, Q be Subset of TOP-REAL 2, p1,p2 be Point of TOP-REAL 2;
assume that
A1: P meets Q & P /\ Q is closed and
A2: 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 Function of I[01], (TOP-REAL 2)|P, s2 be Real st g is
being_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
A3: EX in P /\ Q and
A4: ex g being Function of I[01], (TOP-REAL 2)|P, s2 be Real st g is
being_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,A2,JORDAN5A:22;
EX in P by A3,XBOOLE_0:def 4;
then for g being Function of I[01], (TOP-REAL 2)|P, s2 be Real
st g is
being_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 A4,Th4;
hence thesis by A3;
end;
uniqueness
proof
let IT1, IT2 be Point of TOP-REAL 2;
A5: P /\ Q c= P by XBOOLE_1:17;
assume that
A6: IT1 in P /\ Q and
A7: for g1 being Function of I[01], (TOP-REAL 2)|P, s1 be Real st g1
is being_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 that
A8: IT2 in P /\ Q and
A9: for g2 being Function of I[01], (TOP-REAL 2)|P, s2 be Real st g2
is being_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 Function of I[01], (TOP-REAL 2)|P such that
A10: g is being_homeomorphism and
A11: g.0=p1 & g.1=p2 by A2,TOPREAL1:def 1;
A12: rng g = [#]((TOP-REAL 2)|P) by A10,TOPS_2:def 5
.= P by PRE_TOPC:def 5;
then consider ss1 be object such that
A13: ss1 in dom g and
A14: g.ss1 = IT1 by A5,A6,FUNCT_1:def 3;
reconsider ss1 as Real by A13,BORSUK_1:40;
A15: 0 <= ss1 by A13,BORSUK_1:43;
A16: P /\ Q c= Q & ss1 <= 1 by A13,BORSUK_1:43,XBOOLE_1:17;
consider ss2 be object such that
A17: ss2 in dom g and
A18: g.ss2 = IT2 by A5,A8,A12,FUNCT_1:def 3;
reconsider ss2 as Real by A17,BORSUK_1:40;
A19: 0 <= ss2 by A17,BORSUK_1:43;
A20: ss2 <= 1 by A17,BORSUK_1:43;
per cases by XXREAL_0:1;
suppose
ss1 < ss2;
hence thesis by A7,A8,A10,A11,A14,A18,A15,A16,A20;
end;
suppose
ss1 = ss2;
hence thesis by A14,A18;
end;
suppose
ss1 > ss2;
hence thesis by A6,A9,A10,A11,A14,A18,A16,A19,A20;
end;
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;
assume that
A1: p in P and
A2: P is_an_arc_of p1, p2 and
A3: Q = {p};
A4: P /\ {p} = {p} by A1,ZFMISC_1:46;
A5: for g being Function of I[01], (TOP-REAL 2)|P, s2 be Real st g is
being_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 Function of I[01], (TOP-REAL 2)|P, s2 be Real;
assume that
A6: g is being_homeomorphism and
g.0=p1 and
g.1=p2 and
A7: g.s2=p and
A8: 0<=s2 and
A9: s2<=1;
A10: g is one-to-one by A6,TOPS_2:def 5;
A11: dom g = the carrier of I[01] by A1,FUNCT_2:def 1;
then
A12: s2 in dom g by A8,A9,BORSUK_1:43;
let t be Real;
assume that
A13: 1>=t and
A14: t>s2;
t in dom g by A8,A11,A13,A14,BORSUK_1:43;
then g.t <> g.s2 by A10,A14,A12,FUNCT_1:def 4;
hence thesis by A7,TARSKI:def 1;
end;
A15: P /\ Q is closed by A3,A4,PCOMPS_1:7;
A16: p in P /\ {p} by A4,TARSKI:def 1;
then P meets {p};
hence thesis by A2,A3,A16,A15,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 that
A1: p2 in Q and
A2: P /\ Q is closed and
A3: P is_an_arc_of p1, p2;
A4: for g being Function of I[01], (TOP-REAL 2)|P, s2 be Real st g is
being_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 Function of I[01], (TOP-REAL 2)|P, s2 be Real;
assume that
A5: g is being_homeomorphism and
g.0=p1 and
A6: g.1=p2 & g.s2=p2 and
A7: 0<=s2 & s2<=1;
A8: g is one-to-one by A5,TOPS_2:def 5;
let t be Real;
assume
A9: 1>=t & t>s2;
A10: dom g = [#] I[01] by A5,TOPS_2:def 5
.= the carrier of I[01];
then
A11: 1 in dom g by BORSUK_1:43;
s2 in dom g by A7,A10,BORSUK_1:43;
hence thesis by A6,A11,A8,A9,FUNCT_1:def 4;
end;
p2 in P by A3,TOPREAL1:1;
then p2 in P /\ Q & P meets Q by A1,XBOOLE_0:def 4;
hence thesis by A2,A3,A4,Def2;
end;
theorem Th7:
for P, 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, Q be Subset of TOP-REAL 2, p1,p2 be Point of TOP-REAL 2;
assume that
A1: P c= Q and
A2: P is closed and
A3: P is_an_arc_of p1, p2;
A4: p2 in P by A3,TOPREAL1:1;
P /\ Q = P & p1 in P by A1,A3,TOPREAL1:1,XBOOLE_1:28;
hence thesis by A1,A2,A3,A4,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
q1 in P & q2 in P & for g being
Function of I[01], (TOP-REAL 2)|P, s1, s2 being Real st g is
being_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 Function of I[01], (TOP-REAL 2)|P,
s1, s2 being Real st P
is_an_arc_of p1,p2 & g is being_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
Function of I[01], (TOP-REAL 2)|P, s1,s2 be Real;
assume that
A1: P is_an_arc_of p1,p2 and
A2: g is being_homeomorphism and
A3: g.0=p1 and
A4: g.1=p2 and
A5: g.s1=q1 and
A6: 0<=s1 & s1<=1 and
A7: g.s2=q2 and
A8: 0<=s2 & s2<=1 and
A9: s1<=s2;
reconsider P9 = P as non empty Subset of TOP-REAL 2 by A1,TOPREAL1:1;
s1 in the carrier of I[01] by A6,BORSUK_1:43;
then
A10: q1 in [#]((TOP-REAL 2)|P9) by A5,FUNCT_2:5;
reconsider g as Function of I[01], (TOP-REAL 2)|P9;
s2 in the carrier of I[01] by A8,BORSUK_1:43;
then g.s2 in the carrier of ((TOP-REAL 2)|P9) by FUNCT_2:5;
then
A11: q2 in P by A7,A10,PRE_TOPC:def 5;
A12: now
reconsider s19 = s1, s29 = s2 as Point of I[01] by A6,A8,BORSUK_1:43;
let h be Function of I[01], (TOP-REAL 2)|P9, t1,t2 be Real;
assume that
A13: h is being_homeomorphism and
A14: h.0=p1 and
A15: h.1=p2 and
A16: h.t1=q1 and
A17: 0<=t1 & t1<=1 and
A18: h.t2=q2 and
A19: 0<=t2 & t2<=1;
A20: h is one-to-one by A13,TOPS_2:def 5;
set hg = h"*g;
h" is being_homeomorphism by A13,TOPS_2:56;
then hg is being_homeomorphism by A2,TOPS_2:57;
then
A21: hg is continuous & hg is one-to-one by TOPS_2:def 5;
reconsider hg1 = hg.s19, hg2 = hg.s29 as Real by BORSUK_1:40;
A22: dom g = [#]I[01] by A2,TOPS_2:def 5;
then
A23: 0 in dom g by BORSUK_1:43;
A24: dom h = [#]I[01] by A13,TOPS_2:def 5;
then
A25: t1 in dom h by A17,BORSUK_1:43;
A26: 0 in dom h by A24,BORSUK_1:43;
rng h = [#]((TOP-REAL 2)|P) by A13,TOPS_2:def 5;
then h is onto by FUNCT_2:def 3;
then
A27: h" = (h qua Function)" by A20,TOPS_2:def 4;
then h".p1 = 0 by A14,A26,A20,FUNCT_1:32;
then
A28: (h"*g).0 = 0 by A3,A23,FUNCT_1:13;
s1 in dom g by A6,A22,BORSUK_1:43;
then
A29: (h"*g).s1 = h".q1 by A5,FUNCT_1:13
.= t1 by A16,A20,A25,A27,FUNCT_1:32;
A30: t2 in dom h by A19,A24,BORSUK_1:43;
s2 in dom g by A8,A22,BORSUK_1:43;
then
A31: (h"*g).s2 = h".q2 by A7,FUNCT_1:13
.= t2 by A18,A20,A30,A27,FUNCT_1:32;
A32: 1 in dom g by A22,BORSUK_1:43;
A33: 1 in dom h by A24,BORSUK_1:43;
h".p2 = 1 by A15,A33,A20,A27,FUNCT_1:32;
then
A34: (h"*g).1 = 1 by A4,A32,FUNCT_1:13;
per cases by A9,XXREAL_0:1;
suppose
s1 < s2;
then hg1 < hg2 by A21,A28,A34,JORDAN5A:16;
hence t1 <= t2 by A29,A31;
end;
suppose
s1 = s2;
hence t1 <= t2 by A29,A31;
end;
end;
q1 in P by A10,PRE_TOPC:def 5;
hence thesis by A11,A12;
end;
theorem Th9:
for P being Subset of TOP-REAL 2, p1,p2,q1 being Point of
TOP-REAL 2 st 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: q1 in P;
then reconsider P as non empty Subset of TOP-REAL 2;
now
let g be Function of I[01], (TOP-REAL 2)|P, s1,s2 be Real;
assume that
A2: g is being_homeomorphism and
g.0=p1 and
g.1=p2 and
A3: g.s1=q1 and
A4: 0<=s1 & s1<=1 and
A5: g.s2=q1 and
A6: 0<=s2 & s2<=1;
A7: g is one-to-one by A2,TOPS_2:def 5;
s1 in the carrier of I[01] & s2 in the carrier of I[01] by A4,A6,
BORSUK_1:43;
hence s1 <= s2 by A3,A5,A7,FUNCT_2:19;
end;
hence thesis by A1;
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 that
A1: P is_an_arc_of p1,p2 and
A2: q1 in P;
reconsider P as non empty Subset of TOP-REAL 2 by A2;
A3: now
A4: 0 in the carrier of I[01] by BORSUK_1:43;
let g be Function of I[01], (TOP-REAL 2)|P,s1,s2 be Real;
assume that
A5: g is being_homeomorphism and
A6: g.0=p1 and
g.1=p2 and
A7: g.s1=p1 and
A8: 0<=s1 & s1<=1 and
g.s2=q1 and
A9: 0<=s2 and
s2<=1;
s1 in the carrier of I[01] & g is one-to-one by A5,A8,BORSUK_1:43
,TOPS_2:def 5;
hence s1 <= s2 by A6,A7,A9,A4,FUNCT_2:19;
end;
A10: now
A11: 1 in the carrier of I[01] by BORSUK_1:43;
let g be Function of I[01], (TOP-REAL 2)|P,s1,s2 be Real;
assume that
A12: g is being_homeomorphism and
g.0=p1 and
A13: g.1=p2 and
g.s1=q1 and
0<=s1 and
A14: s1<=1 & g.s2=p2 and
A15: 0<=s2 & s2<=1;
s2 in the carrier of I[01] & g is one-to-one by A12,A15,BORSUK_1:43
,TOPS_2:def 5;
hence s1 <= s2 by A13,A14,A11,FUNCT_2:19;
end;
p1 in P & p2 in P by A1,TOPREAL1:1;
hence thesis by A2,A3,A10;
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:1;
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 that
A1: P is_an_arc_of p1,p2 and
A2: LE q1,q2,P,p1,p2 and
A3: LE q2,q1,P,p1,p2;
consider f being Function of I[01], (TOP-REAL 2)|P such that
A4: f is being_homeomorphism and
A5: f.0 = p1 & f.1 = p2 by A1,TOPREAL1:def 1;
A6: dom f = [#]I[01] by A4,TOPS_2:def 5
.= the carrier of I[01];
A7: rng f = [#]((TOP-REAL 2)|P) by A4,TOPS_2:def 5
.= P by PRE_TOPC:def 5;
then q2 in rng f by A2;
then consider x be object such that
A8: x in dom f and
A9: q2 = f.x by FUNCT_1:def 3;
q1 in rng f by A2,A7;
then consider y be object such that
A10: y in dom f and
A11: q1 = f.y by FUNCT_1:def 3;
[.0,1.] = { r1 where r1 is Real: 0 <= r1 & r1 <= 1 } by RCOMP_1:def 1;
then consider s3 being Real such that
A12: s3 = x and
A13: 0 <= s3 & s3 <= 1 by A6,A8,BORSUK_1:40;
[.0,1.] = { r1 where r1 is Real: 0 <= r1 & r1 <= 1 } by RCOMP_1:def 1;
then consider s4 being Real such that
A14: s4 = y and
A15: 0 <= s4 & s4 <= 1 by A6,A10,BORSUK_1:40;
s3 <= s4 & s4 <= s3 by A2,A3,A4,A5,A9,A12,A13,A11,A14,A15;
hence thesis by A9,A12,A11,A14,XXREAL_0:1;
end;
theorem Th13:
for P being Subset of TOP-REAL 2, p1,p2,q1,q2,q3 being Point of
TOP-REAL 2 st 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 that
A1: LE q1,q2,P,p1,p2 and
A2: LE q2,q3,P,p1,p2;
A3: q2 in P by A1;
A4: now
A5: [.0,1.] = { r1 where r1 is Real: 0 <= r1 & r1 <= 1 }
by RCOMP_1:def 1;
let g be Function of I[01], (TOP-REAL 2)|P,s1,s2 be Real;
assume that
A6: g is being_homeomorphism and
A7: g.0=p1 & g.1=p2 & g.s1=q1 and
0<=s1 and
A8: s1<=1 & g.s2=q3 & 0<=s2 & s2<=1;
rng g = [#]((TOP-REAL 2)|P) by A6,TOPS_2:def 5
.= P by PRE_TOPC:def 5;
then consider x be object such that
A9: x in dom g and
A10: q2 = g.x by A3,FUNCT_1:def 3;
dom g = [#]I[01] by A6,TOPS_2:def 5
.= the carrier of I[01];
then consider s3 being Real such that
A11: s3 = x & 0 <= s3 & s3 <= 1 by A9,A5,BORSUK_1:40;
s1 <= s3 & s3 <= s2 by A1,A2,A6,A7,A8,A10,A11;
hence s1 <= s2 by XXREAL_0:2;
end;
q1 in P & q3 in P by A1,A2;
hence thesis by A4;
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 that
A1: P is_an_arc_of p1,p2 and
A2: q1 in P and
A3: q2 in P and
A4: q1 <> q2;
reconsider P as non empty Subset of TOP-REAL 2 by A2;
not (LE q1,q2,P,p1,p2 iff LE q2,q1,P,p1,p2)
proof
consider f be Function of I[01], (TOP-REAL 2)|P such that
A5: f is being_homeomorphism and
A6: f.0 = p1 & f.1 = p2 by A1,TOPREAL1:def 1;
A7: rng f = [#]((TOP-REAL 2)|P) by A5,TOPS_2:def 5
.= P by PRE_TOPC:def 5;
then consider x be object such that
A8: x in dom f and
A9: q1 = f.x by A2,FUNCT_1:def 3;
consider y be object such that
A10: y in dom f and
A11: q2 = f.y by A3,A7,FUNCT_1:def 3;
dom f = [#]I[01] by A5,TOPS_2:def 5
.= [.0,1.] by BORSUK_1:40;
then reconsider s1 = x, s2 = y as Real by A8,A10;
A12: 0<=s1 by A8,BORSUK_1:43;
A13: s2<=1 by A10,BORSUK_1:43;
A14: 0<=s2 by A10,BORSUK_1:43;
A15: s1<=1 by A8,BORSUK_1:43;
assume
A16: LE q1,q2,P,p1,p2 iff LE q2,q1,P,p1,p2;
per cases by XXREAL_0:1;
suppose
s1 < s2;
hence thesis by A1,A16,A5,A6,A9,A11,A12,A15,A13,Th8;
end;
suppose
s1 = s2;
hence thesis by A4,A9,A11;
end;
suppose
s1 > s2;
hence thesis by A1,A16,A5,A6,A9,A11,A15,A14,A13,Th8;
end;
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 being_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 that
A1: f is being_S-Seq and
A2: L~f /\ Q is closed and
A3: q in L~f and
A4: q in Q;
set P = L~f;
A5: L~f /\ Q c= L~f by XBOOLE_1:17;
set q1 = First_Point(P,f/.1,f/.len f,Q);
L~f meets Q & P is_an_arc_of f/.1,f/.len f by A1,A3,A4,TOPREAL1:25,XBOOLE_0:3
;
then
q1 in L~f /\ Q & for g being Function of I[01], (TOP-REAL 2)| P, s1, s2
being Real
st g is being_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 A2,A4,Def1;
hence thesis by A3,A5;
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 being_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 that
A1: f is being_S-Seq and
A2: L~f /\ Q is closed and
A3: q in L~f and
A4: q in Q;
set q1 = Last_Point(P,f/.1,f/.len f,Q);
A5: L~f /\ Q c= L~f by XBOOLE_1:17;
L~f meets Q & P is_an_arc_of f/.1,f/.len f by A1,A3,A4,TOPREAL1:25,XBOOLE_0:3
;
then
q1 in L~f /\ Q & for g being Function of I[01], (TOP-REAL 2)| P, s1, s2
being Real
st g is being_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 A2,A4,Def2;
hence thesis by A3,A5;
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 p1 <> p2;
then consider f be Function of I[01], (TOP-REAL 2) | LSeg(p1,p2) such that
A1: for x being Real st x in [.0,1.] holds f.x = (1-x)*p1 + x*p2 and
A2: f is being_homeomorphism & f.0 = p1 & f.1 = p2 by JORDAN5A:3;
assume
A3: LE q1, q2, P, p1, p2;
hence q1 in P & q2 in P;
let r1,r2 be Real;
assume that
A4: 0<=r1 and
A5: r1<=1 and
A6: q1=(1-r1)*p1+r1*p2 and
A7: 0<=r2 & r2<=1 and
A8: q2=(1-r2)*p1+r2*p2;
r2 in [.0,1.] by A7,BORSUK_1:40,43;
then
A9: q2 = f.r2 by A8,A1;
r1 in [.0,1.] by A4,A5,BORSUK_1:40,43;
then q1 = f.r1 by A6,A1;
hence thesis by A3,A5,A7,A2,A9;
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 that
A1: P is_an_arc_of p1,p2 and
A2: P /\ Q <> {} and
A3: P /\ Q is closed;
reconsider P as non empty Subset of TOP-REAL 2 by A2;
A4: P meets Q by A2;
A5: P is_an_arc_of p2,p1 by A1,JORDAN5B:14;
A6: for g being Function of I[01], (TOP-REAL 2)|P, s2 being Real st g is
being_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
set Ex = L[01]((0,1)(#),(#)(0,1));
let f be Function of I[01], (TOP-REAL 2)|P, s2 be Real;
assume that
A7: f is being_homeomorphism and
A8: f.0 = p1 and
A9: f.1 = p2 and
A10: f.s2 = Last_Point(P,p2,p1,Q) and
A11: 0<=s2 and
A12: s2<=1;
set s21 = 1 - s2;
set g = f * Ex;
A13: Ex is being_homeomorphism by TREAL_1:18;
dom f = [#]I[01] by A7,TOPS_2:def 5;
then rng Ex = dom f by A13,TOPMETR:20,TOPS_2:def 5;
then dom g = dom Ex by RELAT_1:27;
then
A14: dom g = [#]I[01] by A13,TOPMETR:20,TOPS_2:def 5;
reconsider g as Function of I[01], (TOP-REAL 2) | P by TOPMETR:20;
A15: 1-1 <= s21 & s21 <= 1-0 by A11,A12,XREAL_1:13;
then
A16: s21 in dom g by A14,BORSUK_1:43;
Ex.(#)(0,1) = 1 by BORSUK_1:def 15,TREAL_1:5,9;
then
A17: g.0 = p2 by A9,A14,BORSUK_1:def 14,FUNCT_1:12,TREAL_1:5;
Ex.(0,1)(#) = 0 by BORSUK_1:def 14,TREAL_1:5,9;
then
A18: g.1 = p1 by A8,A14,BORSUK_1:def 15,FUNCT_1:12,TREAL_1:5;
let t be Real;
assume that
A19: 0<=t and
A20: t<s2;
A21: 1-t <= 1-0 by A19,XREAL_1:13;
t <= 1 by A12,A20,XXREAL_0:2;
then
A22: 1-1 <= 1-t by XREAL_1:13;
then reconsider
r2 = 1-s2, t9 = 1-t as Point of Closed-Interval-TSpace(0,1) by A15,A21,
BORSUK_1:43,TOPMETR:20;
A23: 1-t in dom g by A14,A22,A21,BORSUK_1:43;
Ex.r2 = (1-(1-s2))*1 + (1-s2)*0 by BORSUK_1:def 14,def 15,TREAL_1:5,def 3
.= s2;
then
A24: g.s21 = f.s2 by A16,FUNCT_1:12;
Ex.t9 = (1-(1-t))*1 + (1-t)*0 by BORSUK_1:def 14,def 15,TREAL_1:5,def 3
.= t;
then
A25: g.t9 = f.t by A23,FUNCT_1:12;
A26: 1-s2 < 1-t by A20,XREAL_1:15;
g is being_homeomorphism by A7,A13,TOPMETR:20,TOPS_2:57;
hence thesis by A3,A5,A4,A10,A17,A18,A15,A21,A24,A25,A26,Def2;
end;
A27: for g being Function of I[01], (TOP-REAL 2)|P, s2 being Real
st g is
being_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
set Ex = L[01]((0,1)(#),(#)(0,1));
let f be Function of I[01], (TOP-REAL 2)|P, s2 be Real;
assume that
A28: f is being_homeomorphism and
A29: f.0 = p1 and
A30: f.1 = p2 and
A31: f.s2 = First_Point(P,p2,p1,Q) and
A32: 0<=s2 and
A33: s2<=1;
set g = f * Ex;
A34: Ex is being_homeomorphism by TREAL_1:18;
dom f = [#]I[01] by A28,TOPS_2:def 5;
then rng Ex = dom f by A34,TOPMETR:20,TOPS_2:def 5;
then dom g = dom Ex by RELAT_1:27;
then
A35: dom g = [#]I[01] by A34,TOPMETR:20,TOPS_2:def 5;
let t be Real;
assume that
A36: 1>=t and
A37: t>s2;
A38: 1-s2 > 1-t by A37,XREAL_1:15;
set s21 = 1 - s2;
A39: s21 <= 1-0 by A32,XREAL_1:13;
reconsider g as Function of I[01], (TOP-REAL 2) | P by TOPMETR:20;
A40: 1-1 <= 1-t by A36,XREAL_1:13;
A41: 1-t <= 1-0 by A32,A37,XREAL_1:13;
then
A42: 1-t in dom g by A35,A40,BORSUK_1:43;
A43: 1-1 <= s21 by A33,XREAL_1:13;
then
A44: s21 in dom g by A35,A39,BORSUK_1:43;
reconsider r2 = 1-s2, t9 = 1-t as Point of Closed-Interval-TSpace(0,1) by
A43,A39,A40,A41,BORSUK_1:43,TOPMETR:20;
Ex.r2 = (1-(1-s2))*1 + (1-s2)*0 by BORSUK_1:def 14,def 15,TREAL_1:5,def 3
.= s2;
then
A45: g.s21 = f.s2 by A44,FUNCT_1:12;
Ex.t9 = (1-(1-t))*1 + (1-t)*0 by BORSUK_1:def 14,def 15,TREAL_1:5,def 3
.= t;
then
A46: g.t9 = f.t by A42,FUNCT_1:12;
Ex.(#)(0,1) = 1 by BORSUK_1:def 15,TREAL_1:5,9;
then
A47: g.0 = p2 by A30,A35,BORSUK_1:def 14,FUNCT_1:12,TREAL_1:5;
Ex.(0,1)(#) = 0 by BORSUK_1:def 14,TREAL_1:5,9;
then
A48: g.1 = p1 by A29,A35,BORSUK_1:def 15,FUNCT_1:12,TREAL_1:5;
g is being_homeomorphism by A28,A34,TOPMETR:20,TOPS_2:57;
hence thesis by A3,A5,A4,A31,A47,A48,A39,A40,A45,A46,A38,Def1;
end;
Last_Point(P,p2,p1,Q) in P /\ Q & First_Point(P,p2,p1,Q) in P /\ Q by A3,A5
,A4,Def1,Def2;
hence thesis by A1,A3,A4,A6,A27,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
being_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;
assume that
A1: L~f meets Q and
A2: Q is closed and
A3: f is being_S-Seq and
A4: 1 <= i & i+1 <= len f and
A5: First_Point (L~f, f/.1, f/.len f, Q) in LSeg (f, i);
len f >= 2 by A3,TOPREAL1:def 8;
then reconsider
P = L~f, R = LSeg (f, i) as non empty Subset of the carrier of
TOP-REAL 2 by A5,TOPREAL1:23;
A6: P is_an_arc_of f/.1, f/.len f by A3,TOPREAL1:25;
set FPO = First_Point (R, f/.i, f/.(i+1), Q), FPG = First_Point (P, f/.1, f
/.len f, Q);
A7: L~f /\ Q is closed by A2,TOPS_1:8;
then First_Point (P, f/.1, f/.len f, Q) in L~f /\ Q by A1,A6,Def1;
then
A8: First_Point (P, f/.1, f/.len f, Q) in Q by XBOOLE_0:def 4;
A9: i+1 in dom f by A4,SEQ_4:134;
A10: f is one-to-one & i in dom f by A3,A4,SEQ_4:134,TOPREAL1:def 8;
A11: f/.i <> f/.(i+1)
proof
assume f/.i = f/.(i+1);
then i = i+1 by A10,A9,PARTFUN2:10;
hence thesis;
end;
FPG = FPO
proof
FPG in L~f /\ Q by A1,A7,A6,Def1;
then
A12: FPG in L~f by XBOOLE_0:def 4;
consider F be Function of I[01], (TOP-REAL 2)|P such that
A13: F is being_homeomorphism and
A14: F.0 = f/.1 & F.1 = f/.len f by A6,TOPREAL1:def 1;
rng F = [#]((TOP-REAL 2)|P) by A13,TOPS_2:def 5
.= L~f by PRE_TOPC:def 5;
then consider s21 be object such that
A15: s21 in dom F and
A16: F.s21 = FPG by A12,FUNCT_1:def 3;
A17: dom F = [#]I[01] by A13,TOPS_2:def 5
.= [.0,1.] by BORSUK_1:40;
then reconsider s21 as Real by A15;
A18: s21 <= 1 by A15,BORSUK_1:43;
A19: for g being Function of I[01], (TOP-REAL 2)|R, s2 be Real st g is
being_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
consider ppi, pi1 be Real such that
A20: ppi < pi1 and
A21: 0 <= ppi and
ppi <= 1 and
0 <= pi1 and
A22: pi1 <= 1 and
A23: LSeg (f, i) = F.:[.ppi, pi1.] and
A24: F.ppi = f/.i and
A25: F.pi1 = f/.(i+1) by A3,A4,A13,A14,JORDAN5B:7;
A26: ppi in { dd where dd is Real: ppi <= dd & dd <= pi1 } by A20;
then reconsider
Poz = [.ppi, pi1.] as non empty Subset of I[01] by A21,A22,BORSUK_1:40
,RCOMP_1:def 1,XXREAL_1:34;
consider hh be Function of I[01]|Poz, (TOP-REAL 2)|R such that
A27: hh = F|Poz and
A28: hh is being_homeomorphism by A3,A4,A13,A14,A23,JORDAN5B:8;
A29: hh = F * id Poz by A27,RELAT_1:65;
A30: [.ppi,pi1.] c= [.0,1.] by A21,A22,XXREAL_1:34;
reconsider A = Closed-Interval-TSpace (ppi,pi1) as strict SubSpace of
I[01] by A20,A21,A22,TOPMETR:20,TREAL_1:3;
Poz = [#] A by A20,TOPMETR:18;
then
A31: I[01] | Poz = A by PRE_TOPC:def 5;
hh" is being_homeomorphism by A28,TOPS_2:56;
then
A32: hh" is continuous one-to-one by TOPS_2:def 5;
pi1 in { dd where dd is Real: ppi <= dd & dd <= pi1 } by A20;
then pi1 in [.ppi,pi1.] by RCOMP_1:def 1;
then pi1 in dom F /\ Poz by A17,A30,XBOOLE_0:def 4;
then
A33: pi1 in dom hh by A27,RELAT_1:61;
then
A34: hh.pi1 = f/.(i+1) by A25,A27,FUNCT_1:47;
the carrier of ((TOP-REAL 2)|P) = [#] ((TOP-REAL 2)|P)
.= P by PRE_TOPC:def 5;
then reconsider
SEG = LSeg (f, i) as non empty Subset of the carrier of (
TOP-REAL 2)|P by A5,TOPREAL3:19;
A35: the carrier of (((TOP-REAL 2) | P) | SEG) = [#](((TOP-REAL 2) | P) | SEG)
.= SEG by PRE_TOPC:def 5;
reconsider SE = SEG as non empty Subset of TOP-REAL 2;
let g be Function of I[01], (TOP-REAL 2)|R, s2 be Real;
assume that
A36: g is being_homeomorphism and
A37: g.0=f/.i and
A38: g.1=f/.(i+1) and
A39: g.s2 = FPG and
A40: 0<=s2 and
A41: s2<=1;
A42: g is continuous one-to-one by A36,TOPS_2:def 5;
reconsider SEG as non empty Subset of (TOP-REAL 2)|P;
A43: ((TOP-REAL 2) | P) | SEG = (TOP-REAL 2) | SE by GOBOARD9:2;
ppi in [.ppi,pi1.] by A26,RCOMP_1:def 1;
then ppi in dom F /\ Poz by A17,A30,XBOOLE_0:def 4;
then
A44: ppi in dom hh by A27,RELAT_1:61;
then
A45: hh.ppi = f/.i by A24,A27,FUNCT_1:47;
A46: dom hh = [#] (I[01] | Poz) by A28,TOPS_2:def 5;
then
A47: dom hh = Poz by PRE_TOPC:def 5;
A48: rng hh = hh.:(dom hh) by A46,RELSET_1:22
.= [#](((TOP-REAL 2) | P) | SEG) by A23,A35,A27,A47,RELAT_1:129;
let t be Real;
assume that
A49: 0 <= t and
A50: t < s2;
A51: t < 1 by A41,A50,XXREAL_0:2;
then reconsider
w1 = s2, w2 = t as Point of Closed-Interval-TSpace(0,1) by A40,A41,A49,
BORSUK_1:43,TOPMETR:20;
A52: F is one-to-one & rng F = [#]((TOP-REAL 2)|P) by A13,TOPS_2:def 5;
set H = hh" * g;
A53: rng g = [#]((TOP-REAL 2) | SE) by A36,TOPS_2:def 5;
set ss = H.t;
A54: hh is one-to-one by A28,TOPS_2:def 5;
A55: hh is one-to-one by A28,TOPS_2:def 5;
then
A56: dom (hh") = [#] (((TOP-REAL 2) | P) | SEG) by A43,A48,TOPS_2:49;
then
A57: rng H = rng (hh") by A53,RELAT_1:28;
A58: rng (hh") = [#] (I[01] | Poz) by A43,A55,A48,TOPS_2:49
.= Poz by PRE_TOPC:def 5;
then rng H = Poz by A53,A56,RELAT_1:28;
then
A59: rng
H c= the carrier of Closed-Interval-TSpace(ppi,pi1) by A20,TOPMETR:18;
hh is onto by A43,A48,FUNCT_2:def 3;
then
A60: hh" = hh qua Function" by A55,TOPS_2:def 4;
A61: dom g = [#]I[01] by A36,TOPS_2:def 5
.= the carrier of I[01];
then
A62: dom H = the carrier of Closed-Interval-TSpace(0,1) by A43,A53,A56,
RELAT_1:27,TOPMETR:20;
A63: t in dom g by A61,A49,A51,BORSUK_1:43;
then g.t in [#] ((TOP-REAL 2) | SE) by A53,FUNCT_1:def 3;
then
A64: g.t in SEG by PRE_TOPC:def 5;
then consider x be object such that
A65: x in dom F and
A66: x in Poz and
A67: g.t = F.x by A23,FUNCT_1:def 6;
A68: F is one-to-one by A52;
then
A69: (F qua Function)".(g.t) in Poz by A65,A66,A67,FUNCT_1:32;
F is onto by A52,FUNCT_2:def 3;
then
A70: F" = F qua Function" by A52,TOPS_2:def 4;
x = (F qua Function)".(g.t) by A68,A65,A67,FUNCT_1:32;
then F".(g.t) in Poz by A66,A70;
then
A71: F".(g.t) in dom (id Poz) by FUNCT_1:17;
g.t in the carrier of ((TOP-REAL 2)|P) by A64;
then
A72: g.t in dom (F") by A52,TOPS_2:49;
t in dom H by A43,A53,A63,A56,RELAT_1:27;
then
A73: F.ss = (((hh"*g) qua Relation) * (F qua Relation)).t by FUNCT_1:13
.= ( (g qua Relation) * ((hh" qua Relation) * (F qua Relation))).t
by RELAT_1:36
.= (F*hh").(g.t) by A63,FUNCT_1:13
.= ( F * (((F qua Function)" qua Relation) * ((id Poz qua Function)"
qua Relation))).(g.t) by A68,A29,A60,FUNCT_1:44
.= ( ((F" qua Relation) * ((id Poz qua Function)" qua Relation)) * (
F qua Relation)).(g.t) by A70
.= ( (F" qua Relation) * (((id Poz qua Function)" qua Relation) * (F
qua Relation))).(g.t) by RELAT_1:36
.= ( (F" qua Relation) * ((F*id Poz) qua Relation) ).(g.t) by
FUNCT_1:45
.= (F*(id Poz)).(F".(g.t)) by A72,FUNCT_1:13
.= F.((id Poz).(F".(g.t))) by A71,FUNCT_1:13
.= F.((F qua Function)".(g.t)) by A69,A70,FUNCT_1:17
.= g.t by A52,A64,FUNCT_1:35;
1 in dom g by A61,BORSUK_1:43;
then
A74: H.1 = hh".(f/.(i+1)) by A38,FUNCT_1:13
.= pi1 by A54,A33,A34,A60,FUNCT_1:32;
0 in dom g by A61,BORSUK_1:43;
then
A75: H.0 = hh".(f/.i) by A37,FUNCT_1:13
.= ppi by A54,A44,A45,A60,FUNCT_1:32;
dom H = dom g by A43,A53,A56,RELAT_1:27;
then ss in Poz by A58,A63,A57,FUNCT_1:def 3;
then ss in { l where l is Real: ppi <= l & l <= pi1 }
by RCOMP_1:def 1;
then consider ss9 be Real such that
A76: ss9 = ss and
A77: ppi <= ss9 and
ss9 <= pi1;
reconsider H as Function of Closed-Interval-TSpace(0,1),
Closed-Interval-TSpace(ppi,pi1) by A62,A59,FUNCT_2:2;
A78: ss9 = H.w2 by A76;
ex z be object st z in dom F & z in Poz & F.s21 = F.z by A5,A16,A23,
FUNCT_1:def 6;
then
A79: s21 in Poz by A15,A68,FUNCT_1:def 4;
then hh.s21 = g.s2 by A16,A39,A27,FUNCT_1:49;
then s21 = (hh qua Function)".(g.s2) by A55,A47,A79,FUNCT_1:32;
then
A80: s21 = hh".(g.s2) by A60;
s2 in dom g by A40,A41,A61,BORSUK_1:43;
then s21 = H.w1 by A80,FUNCT_1:13;
then ss9 < s21 by A20,A50,A75,A74,A42,A32,A31,A78,JORDAN5A:15,TOPMETR:20;
hence thesis by A1,A7,A6,A13,A14,A16,A18,A21,A76,A77,A73,Def1;
end;
A81: LSeg (f, i) /\ Q is closed by A2,TOPS_1:8;
LSeg (f, i) /\ Q <> {} by A5,A8,XBOOLE_0:def 4;
then
A82: LSeg (f, i) meets Q;
LSeg (f,i) = LSeg (f/.i, f/.(i+1)) by A4,TOPREAL1:def 3;
then
A83: R is_an_arc_of f/.i, f/.(i+1) by A11,TOPREAL1:9;
FPG in LSeg (f,i) /\ Q by A5,A8,XBOOLE_0:def 4;
hence thesis by A82,A81,A83,A19,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
being_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;
assume that
A1: L~f meets Q and
A2: Q is closed and
A3: f is being_S-Seq and
A4: 1 <= i & i+1 <= len f and
A5: Last_Point (L~f, f/.1, f/.len f, Q) in LSeg (f, i);
len f >= 2 by A3,TOPREAL1:def 8;
then reconsider
P = L~f, R = LSeg (f, i) as non empty Subset of TOP-REAL 2 by A5,TOPREAL1:23;
A6: P is_an_arc_of f/.1, f/.len f by A3,TOPREAL1:25;
set FPO = Last_Point (R, f/.i, f/.(i+1), Q), FPG = Last_Point (P, f/.1, f/.
len f, Q);
A7: L~f /\ Q is closed by A2,TOPS_1:8;
then Last_Point (P, f/.1, f/.len f, Q) in L~f /\ Q by A1,A6,Def2;
then
A8: Last_Point (P, f/.1, f/.len f, Q) in Q by XBOOLE_0:def 4;
A9: i+1 in dom f by A4,SEQ_4:134;
A10: f is one-to-one & i in dom f by A3,A4,SEQ_4:134,TOPREAL1:def 8;
A11: f/.i <> f/.(i+1)
proof
assume f/.i = f/.(i+1);
then i = i+1 by A10,A9,PARTFUN2:10;
hence thesis;
end;
FPG = FPO
proof
FPG in L~f /\ Q by A1,A7,A6,Def2;
then
A12: FPG in L~f by XBOOLE_0:def 4;
consider F be Function of I[01], (TOP-REAL 2)|P such that
A13: F is being_homeomorphism and
A14: F.0 = f/.1 & F.1 = f/.len f by A6,TOPREAL1:def 1;
rng F = [#]((TOP-REAL 2)|P) by A13,TOPS_2:def 5
.= L~f by PRE_TOPC:def 5;
then consider s21 be object such that
A15: s21 in dom F and
A16: F.s21 = FPG by A12,FUNCT_1:def 3;
A17: dom F = [#]I[01] by A13,TOPS_2:def 5
.= [.0,1.] by BORSUK_1:40;
then reconsider s21 as Real by A15;
A18: 0 <= s21 & s21 <= 1 by A15,BORSUK_1:43;
A19: for g being Function of I[01], (TOP-REAL 2)|R, s2 be Real st g is
being_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
consider ppi, pi1 be Real such that
A20: ppi < pi1 and
A21: 0 <= ppi and
ppi <= 1 and
0 <= pi1 and
A22: pi1 <= 1 and
A23: LSeg (f, i) = F.:[.ppi, pi1.] and
A24: F.ppi = f/.i and
A25: F.pi1 = f/.(i+1) by A3,A4,A13,A14,JORDAN5B:7;
A26: ppi in { dd where dd is Real: ppi <= dd & dd <= pi1 } by A20;
then reconsider
Poz = [.ppi, pi1.] as non empty Subset of I[01] by A21,A22,BORSUK_1:40
,RCOMP_1:def 1,XXREAL_1:34;
A27: [.ppi,pi1.] c= [.0,1.] by A21,A22,XXREAL_1:34;
reconsider A = Closed-Interval-TSpace (ppi,pi1) as strict SubSpace of
I[01] by A20,A21,A22,TOPMETR:20,TREAL_1:3;
A28: Poz = [#] A by A20,TOPMETR:18;
then
A29: I[01] | Poz = A by PRE_TOPC:def 5;
Closed-Interval-TSpace (ppi,pi1) is compact by A20,HEINE:4;
then [#] Closed-Interval-TSpace (ppi,pi1) is compact by COMPTS_1:1;
then for P being Subset of A st P=Poz holds P is compact by A20,
TOPMETR:18;
then Poz is compact by A28,COMPTS_1:2;
then
A30: I[01]|Poz is compact by COMPTS_1:3;
reconsider Lf = L~f as non empty Subset of TOP-REAL 2 by A6;
let g be Function of I[01], (TOP-REAL 2)|R, s2 be Real;
assume that
A31: g is being_homeomorphism and
A32: g.0=f/.i and
A33: g.1=f/.(i+1) and
A34: g.s2 = FPG and
A35: 0<=s2 and
A36: s2<=1;
the carrier of ((TOP-REAL 2)|Lf) = [#] ((TOP-REAL 2)|Lf)
.= Lf by PRE_TOPC:def 5;
then reconsider
SEG = LSeg (f, i) as non empty Subset of (TOP-REAL 2)|Lf by A5,
TOPREAL3:19;
reconsider SE = SEG as non empty Subset of TOP-REAL 2;
A37: rng g = [#]((TOP-REAL 2) | SE) by A31,TOPS_2:def 5;
set gg = F | Poz;
A38: the carrier of (I[01]|Poz) = [#] (I[01]|Poz) .= Poz by PRE_TOPC:def 5;
then reconsider gg as Function of I[01]|Poz, (TOP-REAL 2)| P by
FUNCT_2:32;
let t be Real;
assume that
A39: 1 >= t and
A40: t > s2;
A41: rng gg c= SEG
proof
let ii be object;
assume ii in rng gg;
then consider j be object such that
A42: j in dom gg and
A43: ii = gg.j by FUNCT_1:def 3;
j in dom F /\ Poz by A42,RELAT_1:61;
then j in dom F by XBOOLE_0:def 4;
then F.j in LSeg (f,i) by A23,A38,A42,FUNCT_1:def 6;
hence thesis by A38,A42,A43,FUNCT_1:49;
end;
A44: the carrier of (((TOP-REAL 2) | Lf) | SEG) = [#](((TOP-REAL 2) | Lf
) | SEG)
.= SEG by PRE_TOPC:def 5;
reconsider SEG as non empty Subset of (TOP-REAL 2)|Lf;
reconsider hh9 = gg as Function of I[01]|Poz, ((TOP-REAL 2) | Lf)| SEG
by A44,A41,FUNCT_2:6;
reconsider hh = hh9 as Function of I[01]|Poz, (TOP-REAL 2) | SE by
GOBOARD9:2;
A45: dom hh = [#] (I[01] | Poz) by FUNCT_2:def 1;
then
A46: dom hh = Poz by PRE_TOPC:def 5;
A47: rng hh = hh.:(dom hh) by A45,RELSET_1:22
.= [#](((TOP-REAL 2) | Lf) | SEG) by A23,A44,A46,RELAT_1:129;
A48: F is one-to-one by A13,TOPS_2:def 5;
then
A49: hh is one-to-one by FUNCT_1:52;
set H = hh" * g;
A50: ((TOP-REAL 2) | Lf) | SEG = (TOP-REAL 2) | SE by GOBOARD9:2;
A51: hh9 is one-to-one by A48,FUNCT_1:52;
then
A52: dom (hh") = [#] (((TOP-REAL 2) | Lf) | SEG) by A50,A47,TOPS_2:49;
then
A53: rng H = rng (hh") by A37,RELAT_1:28;
A54: dom g = [#]I[01] by A31,TOPS_2:def 5
.= the carrier of I[01];
then
A55: dom H = the carrier of Closed-Interval-TSpace(0,1) by A50,A37,A52,
RELAT_1:27,TOPMETR:20;
A56: t in dom g by A35,A54,A39,A40,BORSUK_1:43;
then g.t in [#] ((TOP-REAL 2) | SE) by A37,FUNCT_1:def 3;
then
A57: g.t in SEG by PRE_TOPC:def 5;
then consider x be object such that
A58: x in dom F and
A59: x in Poz and
A60: g.t = F.x by A23,FUNCT_1:def 6;
hh is onto by A50,A47,FUNCT_2:def 3;
then
A61: hh" = hh qua Function" by A51,TOPS_2:def 4;
A62: (F qua Function)".(g.t) in Poz by A48,A58,A59,A60,FUNCT_1:32;
ex z be object st z in dom F & z in Poz & F.s21 = F.z by A5,A16,A23,
FUNCT_1:def 6;
then
A63: s21 in Poz by A15,A48,FUNCT_1:def 4;
then hh.s21 = g.s2 by A16,A34,FUNCT_1:49;
then s21 = (hh qua Function)".(g.s2) by A51,A46,A63,FUNCT_1:32;
then
A64: s21 = hh".(g.s2) by A61;
A65: g is continuous one-to-one by A31,TOPS_2:def 5;
A66: (TOP-REAL 2)|SE is T_2 by TOPMETR:2;
reconsider w1 = s2, w2 = t as Point of Closed-Interval-TSpace(0,1) by A35
,A36,A39,A40,BORSUK_1:43,TOPMETR:20;
A67: hh = F * id Poz by RELAT_1:65;
set ss = H.t;
A68: F is one-to-one & rng F = [#]((TOP-REAL 2)|P) by A13,TOPS_2:def 5;
A69: rng (hh") = [#] (I[01] | Poz) by A50,A51,A47,TOPS_2:49
.= Poz by PRE_TOPC:def 5;
then rng H = Poz by A37,A52,RELAT_1:28;
then
A70: rng H c= the carrier of Closed-Interval-TSpace(ppi,pi1) by A20,TOPMETR:18
;
dom H = dom g by A50,A37,A52,RELAT_1:27;
then ss in Poz by A69,A56,A53,FUNCT_1:def 3;
then ss in { l where l is Real: ppi <= l & l <= pi1 }
by RCOMP_1:def 1;
then consider ss9 be Real such that
A71: ss9 = ss and
ppi <= ss9 and
A72: ss9 <= pi1;
F is onto by A68,FUNCT_2:def 3;
then
A73: F" = F qua Function" by A68,TOPS_2:def 4;
A74: 1 >= ss9 by A22,A72,XXREAL_0:2;
x = (F qua Function)".(g.t) by A48,A58,A60,FUNCT_1:32;
then F".(g.t) in Poz by A59,A73;
then
A75: F".(g.t) in dom (id Poz) by FUNCT_1:17;
g.t in the carrier of ((TOP-REAL 2)|Lf) by A57;
then
A76: g.t in dom (F") by A68,TOPS_2:49;
t in dom H by A50,A37,A56,A52,RELAT_1:27;
then
A77: F.ss = (((hh"*g) qua Relation) * (F qua Relation)).t by FUNCT_1:13
.= ( (g qua Relation) * ((hh" qua Relation) * (F qua Relation))).t
by RELAT_1:36
.= (F*hh").(g.t) by A56,FUNCT_1:13
.= (F*(hh qua Function)").(g.t) by A61
.= ( F * (((F qua Function)" qua Relation) * ((id Poz qua Function)"
qua Relation))).(g.t) by A48,A67,FUNCT_1:44
.= ( ((F" qua Relation) * ((id Poz qua Function)" qua Relation)) * (
F qua Relation)).(g.t) by A73
.= ( (F" qua Relation) * (((id Poz qua Function)" qua Relation) * (F
qua Relation))).(g.t) by RELAT_1:36
.= ( (F" qua Relation) * ((F*id Poz) qua Relation) ).(g.t) by
FUNCT_1:45
.= (F*(id Poz)).(F".(g.t)) by A76,FUNCT_1:13
.= F.((id Poz).(F".(g.t))) by A75,FUNCT_1:13
.= F.((id Poz).((F qua Function)".(g.t))) by A73
.= F.((F qua Function)".(g.t)) by A62,FUNCT_1:17
.= g.t by A68,A57,FUNCT_1:35;
pi1 in { dd where dd is Real: ppi <= dd & dd <= pi1 } by A20;
then pi1 in [.ppi,pi1.] by RCOMP_1:def 1;
then pi1 in dom F /\ Poz by A17,A27,XBOOLE_0:def 4;
then
A78: pi1 in dom hh by RELAT_1:61;
then
A79: hh.pi1 = f/.(i+1) by A25,FUNCT_1:47;
F is continuous by A13,TOPS_2:def 5;
then gg is continuous by TOPMETR:7;
then hh is being_homeomorphism by A50,A51,A47,A30,A66,COMPTS_1:17
,TOPMETR:6;
then hh" is being_homeomorphism by TOPS_2:56;
then
A80: hh" is continuous one-to-one by TOPS_2:def 5;
ppi in [.ppi,pi1.] by A26,RCOMP_1:def 1;
then ppi in dom F /\ Poz by A17,A27,XBOOLE_0:def 4;
then
A81: ppi in dom hh by RELAT_1:61;
then
A82: hh.ppi = f/.i by A24,FUNCT_1:47;
1 in dom g by A54,BORSUK_1:43;
then
A83: H.1 = hh".(f/.(i+1)) by A33,FUNCT_1:13
.= pi1 by A49,A78,A79,A61,FUNCT_1:32;
0 in dom g by A54,BORSUK_1:43;
then
A84: H.0 = hh".(f/.i) by A32,FUNCT_1:13
.= ppi by A49,A81,A82,A61,FUNCT_1:32;
reconsider H as Function of Closed-Interval-TSpace(0,1),
Closed-Interval-TSpace(ppi,pi1) by A55,A70,FUNCT_2:2;
s2 in dom g by A35,A36,A54,BORSUK_1:43;
then
A85: s21 = H.w1 by A64,FUNCT_1:13;
ss9 = H.w2 by A71;
then ss9 > s21 by A20,A40,A84,A83,A65,A80,A29,A85,JORDAN5A:15,TOPMETR:20;
hence thesis by A1,A7,A6,A13,A14,A16,A18,A71,A74,A77,Def2;
end;
A86: LSeg (f, i) /\ Q is closed by A2,TOPS_1:8;
LSeg (f, i) /\ Q <> {} by A5,A8,XBOOLE_0:def 4;
then
A87: LSeg (f, i) meets Q;
LSeg (f,i) = LSeg (f/.i, f/.(i+1)) by A4,TOPREAL1:def 3;
then
A88: R is_an_arc_of f/.i, f/.(i+1) by A11,TOPREAL1:9;
FPG in LSeg (f,i) /\ Q by A5,A8,XBOOLE_0:def 4;
hence thesis by A87,A86,A88,A19,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 being_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 that
A1: 1 <= i & i+1 <= len f and
A2: f is being_S-Seq and
A3: First_Point ( L~f, f/.1, f/.len f, LSeg (f,i) ) in LSeg (f,i);
reconsider Q = LSeg (f,i) as non empty Subset of TOP-REAL 2 by A3;
Q = LSeg (f/.i, f/.(i+1)) by A1,TOPREAL1:def 3;
then Q c= L~f by A1,SPPOL_2:16;
then L~f meets Q by A3,XBOOLE_0:3;
then
A4: First_Point (L~f, f/.1, f/.len f, Q) = First_Point (Q, f/.i, f/.(i+1), Q
) by A1,A2,A3,Th19;
Q is closed & Q is_an_arc_of f/.i, f/.(i+1) by A1,A2,JORDAN5B:15;
hence thesis by A4,Th7;
end;
theorem
for f being FinSequence of TOP-REAL 2, i be Nat st 1 <= i &
i+1 <= len f & f is being_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 that
A1: 1 <= i & i+1 <= len f and
A2: f is being_S-Seq and
A3: Last_Point ( L~f, f/.1, f/.len f, LSeg (f,i) ) in LSeg (f,i);
reconsider Q = LSeg (f,i) as non empty Subset of TOP-REAL 2 by A3;
Q = LSeg (f/.i, f/.(i+1)) by A1,TOPREAL1:def 3;
then Q c= L~f by A1,SPPOL_2:16;
then L~f meets Q by A3,XBOOLE_0:3;
then
A4: Last_Point (L~f, f/.1, f/.len f, Q) = Last_Point (Q, f/.i, f/.(i+1), Q)
by A1,A2,A3,Th20;
Q is closed & Q is_an_arc_of f/.i, f/.(i+1) by A1,A2,JORDAN5B:15;
hence thesis by A4,Th7;
end;
theorem Th23:
for f be FinSequence of TOP-REAL 2, i be Nat st f is
being_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 that
A1: f is being_S-Seq and
A2: 1 <= i & i+1 <= len f;
set p1 = f/.1, p2 = f/.len f, q1 = f/.i, q2 = f/.(i+1);
A3: len f >= 2 by A1,TOPREAL1:def 8;
then reconsider P = L~f as non empty Subset of TOP-REAL 2 by TOPREAL1:23;
i+1 in dom f by A2,SEQ_4:134;
then
A4: q2 in P by A3,GOBOARD1:1;
A5: for g being Function of I[01], (TOP-REAL 2)|P, s1,s2 be Real
st g is
being_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 Function of I[01], (TOP-REAL 2)|P, s1,s2 be Real;
assume that
A6: g is being_homeomorphism and
A7: g.0 = p1 & g.1 = p2 and
A8: g.s1 = q1 and
A9: 0 <= s1 & s1 <= 1 and
A10: g.s2 = q2 and
A11: 0 <= s2 & s2 <= 1;
A12: dom g = [#]I[01] by A6,TOPS_2:def 5
.= the carrier of I[01];
then
A13: s1 in dom g by A9,BORSUK_1:43;
A14: s2 in dom g by A11,A12,BORSUK_1:43;
A15: g is one-to-one by A6,TOPS_2:def 5;
consider r1, r2 be Real such that
A16: r1 < r2 and
A17: 0 <= r1 and
A18: r1 <= 1 and
0 <= r2 and
A19: r2 <= 1 and
LSeg (f, i) = g.:[.r1, r2.] and
A20: g.r1 = q1 and
A21: g.r2 = q2 by A1,A2,A6,A7,JORDAN5B:7;
A22: r2 in dom g by A16,A17,A19,A12,BORSUK_1:43;
r1 in dom g by A17,A18,A12,BORSUK_1:43;
then s1 = r1 by A8,A20,A13,A15,FUNCT_1:def 4;
hence thesis by A10,A16,A21,A22,A14,A15,FUNCT_1:def 4;
end;
i in dom f by A2,SEQ_4:134;
then q1 in P by A3,GOBOARD1:1;
hence thesis by A4,A5;
end;
theorem Th24:
for f be FinSequence of TOP-REAL 2, i, j be Nat st f is being_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 being_S-Seq and
A2: 1 <= i and
A3: i <= j and
A4: j <= len f;
consider k being Nat such that
A5: i+k = j by A3,NAT_1:10;
A6: len f >= 2 by A1,TOPREAL1:def 8;
then reconsider P = L~f as non empty Subset of TOP-REAL 2 by TOPREAL1:23;
defpred ILE[Nat] means 1 <= i & i+$1 <= len f implies LE f/.i, f
/.(i+$1), P, f/.1, f/.len f;
A7: for l be Nat st ILE[l] holds ILE[l + 1]
proof
let l be Nat;
assume
A8: ILE[l];
A9: i+l <= i+l+1 by NAT_1:11;
assume that
A10: 1 <= i and
A11: i+(l+1) <= len f;
A12: i+l+1 <= len f by A11;
i <= i+l by NAT_1:11;
then 1 <= i+l by A10,XXREAL_0:2;
then LE f/.(i+l), f/.(i+(l+1)), P, f/.1,f/.len f by A1,A12,Th23;
hence thesis by A8,A10,A11,A9,Th13,XXREAL_0:2;
end;
A13: ILE[0]
proof
assume 1 <= i & i+0 <= len f;
then i in dom f by FINSEQ_3:25;
hence thesis by A6,Th9,GOBOARD1:1;
end;
A14: for l be Nat holds ILE[l] from NAT_1:sch 2(A13, A7);
thus thesis by A2,A4,A5,A14;
end;
Lm1: 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
being_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 that
A1: LSeg(f,i) meets Q and
A2: f is being_S-Seq and
A3: Q is closed and
A4: 1<=i & i+1<=len f and
A5: q in LSeg(f,i) and
A6: q in Q;
reconsider P = LSeg(f,i) as non empty Subset of TOP-REAL 2 by A5;
set q1 = First_Point(P,f/.i,f/.(i+1),Q), p1 = f/.i, p2 = f/.(i+1);
A7: P /\ Q c= P by XBOOLE_1:17;
A8: i+1 in dom f by A4,SEQ_4:134;
A9: f is one-to-one & i in dom f by A2,A4,SEQ_4:134,TOPREAL1:def 8;
A10: p1 <> p2
proof
assume p1 = p2;
then i = i+1 by A9,A8,PARTFUN2:10;
hence thesis;
end;
A11: P /\ Q is closed by A3,TOPS_1:8;
P is_an_arc_of f/.i,f/.(i+1) by A2,A4,JORDAN5B:15;
then
q1 in P /\ Q & for g being Function of I[01], (TOP-REAL 2)|P,
s1, s2 being Real
st g is being_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,A6,A11,Def1;
then
A12: LE q1, q, P, p1, p2 by A5,A7;
LSeg(f,i) = LSeg(f/.i, f/.(i+1)) by A4,TOPREAL1:def 3;
hence thesis by A10,A12,Th17;
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 L~f meets Q & f is
being_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 that
A1: L~f meets Q and
A2: f is being_S-Seq and
A3: Q is closed and
A4: First_Point(L~f,f/.1,f/.len f,Q) in LSeg(f,i) and
A5: 1<=i & i+1<=len f and
A6: q in LSeg(f,i) & q in Q;
len f >= 2 by A2,TOPREAL1:def 8;
then reconsider
P = L~f, R = LSeg (f,i) as non empty Subset of TOP-REAL 2 by A4,TOPREAL1:23;
LSeg (f,i) /\ Q <> {} by A6,XBOOLE_0:def 4;
then
A7: LSeg (f,i) meets Q;
First_Point (P,f/.1,f/.len f,Q) = First_Point (R, f/.i, f/.(i+1), Q) by A1,A2
,A3,A4,A5,Th19;
hence thesis by A2,A3,A5,A6,A7,Lm1;
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 LSeg (f,i) meets Q & f is
being_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 that
A1: LSeg(f,i) meets Q and
A2: f is being_S-Seq and
A3: Q is closed and
A4: 1<=i & i+1<=len f and
A5: q in LSeg(f,i) and
A6: q in Q;
reconsider P = LSeg(f,i) as non empty Subset of TOP-REAL 2 by A5;
set q1 = Last_Point(P,f/.i,f/.(i+1),Q), p1 = f/.i, p2 = f/.(i+1);
A7: P /\ Q c= P by XBOOLE_1:17;
A8: i+1 in dom f by A4,SEQ_4:134;
A9: f is one-to-one & i in dom f by A2,A4,SEQ_4:134,TOPREAL1:def 8;
A10: p1 <> p2
proof
assume p1 = p2;
then i = i+1 by A9,A8,PARTFUN2:10;
hence thesis;
end;
A11: P /\ Q is closed by A3,TOPS_1:8;
P is_an_arc_of f/.i,f/.(i+1) by A2,A4,JORDAN5B:15;
then
q1 in P /\ Q & for g being Function of I[01], (TOP-REAL 2)|P,
s1, s2 be Real
st g is being_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,A6,A11,Def2;
then
A12: LE q, q1, P, p1, p2 by A5,A7;
LSeg(f,i) = LSeg(f/.i, f/.(i+1)) by A4,TOPREAL1:def 3;
hence thesis by A10,A12,Th17;
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 L~f meets Q & f is
being_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 that
A1: L~f meets Q and
A2: f is being_S-Seq and
A3: Q is closed and
A4: Last_Point(L~f,f/.1,f/.len f,Q) in LSeg(f,i) and
A5: 1<=i & i+1<=len f and
A6: q in LSeg(f,i) & q in Q;
len f >= 2 by A2,TOPREAL1:def 8;
then reconsider
P = L~f, R = LSeg (f,i) as non empty Subset of TOP-REAL 2 by A4,TOPREAL1:23;
LSeg (f,i) /\ Q <> {} by A6,XBOOLE_0:def 4;
then
A7: LSeg (f,i) meets Q;
Last_Point(P,f/.1,f/.len f,Q) = Last_Point (R, f/.i, f/.(i+1), Q) by A1,A2,A3
,A4,A5,Th20;
hence thesis by A2,A3,A5,A6,A7,Lm3;
end;
theorem Th25:
for f being FinSequence of TOP-REAL 2, q being Point of TOP-REAL
2, i being Nat st f is being_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 that
A1: f is being_S-Seq and
A2: 1<=i & i+1<=len f and
A3: q in LSeg(f,i);
set p1 = f/.1, p2 = f/.len f, q1 = f/.i;
A4: 2 <= len f by A1,TOPREAL1:def 8;
then reconsider P = L~f as non empty Subset of TOP-REAL 2 by TOPREAL1:23;
i in dom f by A2,SEQ_4:134;
then
A5: q1 in P by A4,GOBOARD1:1;
A6: for g being Function of I[01], (TOP-REAL 2)|P,
s1,s2 be Real st g is
being_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 Function of I[01], (TOP-REAL 2)|P, s1,s2 be Real;
assume that
A7: g is being_homeomorphism and
A8: g.0=p1 & g.1=p2 and
A9: g.s1=q1 and
A10: 0<=s1 & s1<=1 and
A11: g.s2=q and
A12: 0<=s2 & s2<=1;
A13: dom g = [#]I[01] by A7,TOPS_2:def 5
.= the carrier of I[01];
then
A14: s1 in dom g by A10,BORSUK_1:43;
consider r1, r2 be Real such that
r1 < r2 and
A15: 0 <= r1 & r1 <= 1 and
0 <= r2 and
r2 <= 1 and
A16: LSeg (f, i) = g.: [.r1, r2.] and
A17: g.r1 = q1 and
g.r2 = f/.(i+1) by A1,A2,A7,A8,JORDAN5B:7;
consider r39 be object such that
A18: r39 in dom g and
A19: r39 in [.r1, r2.] and
A20: g.r39 = q by A3,A16,FUNCT_1:def 6;
r39 in { l where l is Real: r1 <= l & l <= r2 }
by A19,RCOMP_1:def 1;
then consider r3 be Real such that
A21: r3 = r39 and
A22: r1 <= r3 and
r3 <= r2;
A23: g is one-to-one by A7,TOPS_2:def 5;
A24: r1 in dom g by A15,A13,BORSUK_1:43;
s2 in dom g by A12,A13,BORSUK_1:43;
then s2 = r3 by A11,A18,A20,A21,A23,FUNCT_1:def 4;
hence thesis by A9,A17,A22,A24,A14,A23,FUNCT_1:def 4;
end;
q in P by A3,SPPOL_2:17;
hence thesis by A5,A6;
end;
theorem Th26:
for f being FinSequence of TOP-REAL 2, q being Point of TOP-REAL
2, i being Nat st f is being_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 that
A1: f is being_S-Seq and
A2: 1<=i & i+1<=len f and
A3: q in LSeg(f,i);
len f >= 2 by A1,TOPREAL1:def 8;
then reconsider P = L~f as non empty Subset of TOP-REAL 2 by TOPREAL1:23;
set p1 = f/.1, p2 = f/.len f, q1 = f/.(i+1);
q1 in LSeg (f,i) by A2,TOPREAL1:21;
then
A4: q1 in P by SPPOL_2:17;
A5: for g being Function of I[01], (TOP-REAL 2)|P,
s1,s2 be Real st g is
being_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 Function of I[01], (TOP-REAL 2)|P, s1,s2 be Real;
assume that
A6: g is being_homeomorphism and
A7: g.0=p1 & g.1=p2 and
A8: g.s1=q and
A9: 0<=s1 & s1<=1 and
A10: g.s2=q1 and
A11: 0<=s2 & s2<=1;
A12: dom g = [#]I[01] by A6,TOPS_2:def 5
.= the carrier of I[01];
then
A13: s2 in dom g by A11,BORSUK_1:43;
consider r1, r2 be Real such that
A14: r1 < r2 & 0 <= r1 and
r1 <= 1 and
0 <= r2 and
A15: r2 <= 1 and
A16: LSeg (f, i) = g.:[.r1, r2.] and
g.r1 = f/.i and
A17: g.r2 = q1 by A1,A2,A6,A7,JORDAN5B:7;
A18: r2 in dom g by A14,A15,A12,BORSUK_1:43;
consider r39 be object such that
A19: r39 in dom g and
A20: r39 in [.r1, r2.] and
A21: g.r39 = q by A3,A16,FUNCT_1:def 6;
r39 in { l where l is Real: r1 <= l & l <= r2 }
by A20,RCOMP_1:def 1;
then consider r3 be Real such that
A22: r3 = r39 and
r1 <= r3 and
A23: r3 <= r2;
A24: g is one-to-one by A6,TOPS_2:def 5;
s1 in dom g by A9,A12,BORSUK_1:43;
then s1 = r3 by A8,A19,A21,A22,A24,FUNCT_1:def 4;
hence thesis by A10,A17,A23,A18,A13,A24,FUNCT_1:def 4;
end;
q in P by A3,SPPOL_2:17;
hence thesis by A4,A5;
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
being_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 that
A1: L~f meets Q and
A2: f is being_S-Seq and
A3: Q is closed and
A4: First_Point(L~f,f/.1,f/.len f,Q) in LSeg(f,i) and
A5: 1<=i and
A6: i+1<=len f and
A7: q in LSeg(f,j) and
A8: 1<=j & j+1<=len f and
A9: q in Q and
A10: First_Point (L~f,f/.1,f/.len f,Q) <> q;
reconsider P = L~f as non empty Subset of TOP-REAL 2 by A4,SPPOL_2:17;
set q1 = First_Point(P,f/.1,f/.len f,Q), p1 = f/.i;
A11: q in L~f by A7,SPPOL_2:17;
thus i <= j
proof
L~f /\ Q is closed by A3,TOPS_1:8;
then
A12: LE q1, q, P, f/.1, f/.len f by A2,A9,A11,Th15;
A13: LE q, f/.(j+1), P, f/.1, f/.len f by A2,A7,A8,Th26;
i <= i + 1 by NAT_1:11;
then
A14: i <= len f by A6,XXREAL_0:2;
assume j < i;
then
A15: j+1 <= i by NAT_1:13;
1 <= j+1 by NAT_1:11;
then LE f/.(j+1), p1, P, f/.1, f/.len f by A2,A15,A14,Th24;
then
A16: LE q, p1, P, f/.1, f/.len f by A13,Th13;
LE p1, q1, P, f/.1, f/.len f by A2,A4,A5,A6,Th25;
then LE q, q1, P, f/.1, f/.len f by A16,Th13;
hence contradiction by A2,A10,A12,Th12,TOPREAL1:25;
end;
assume i = j;
hence thesis by A1,A2,A3,A4,A5,A6,A7,A9,Lm2;
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
being_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 that
A1: L~f meets Q and
A2: f is being_S-Seq and
A3: Q is closed and
A4: Last_Point(L~f,f/.1,f/.len f,Q) in LSeg(f,i) and
A5: 1<=i & i+1<=len f and
A6: q in LSeg(f,j) and
A7: 1<=j and
A8: j+1<=len f and
A9: q in Q and
A10: Last_Point (L~f,f/.1,f/.len f,Q) <> q;
reconsider P = L~f as non empty Subset of TOP-REAL 2 by A4,SPPOL_2:17;
set q1 = Last_Point(P,f/.1,f/.len f,Q), p2 = f/.(i+1);
A11: q in L~f by A6,SPPOL_2:17;
thus i >= j
proof
assume j > i;
then
A12: i+1 <= j by NAT_1:13;
j <= j + 1 by NAT_1:11;
then 1 <= i + 1 & j <= len f by A8,NAT_1:11,XXREAL_0:2;
then
A13: LE p2, f/.j, P, f/.1, f/.len f by A2,A12,Th24;
LE f/.j, q, P, f/.1, f/.len f by A2,A6,A7,A8,Th25;
then
A14: LE p2, q, P, f/.1, f/.len f by A13,Th13;
L~f /\ Q is closed by A3,TOPS_1:8;
then
A15: LE q, q1, P, f/.1, f/.len f by A2,A9,A11,Th16;
LE q1, p2, P, f/.1, f/.len f by A2,A4,A5,Th26;
then LE q1, q, P, f/.1, f/.len f by A14,Th13;
hence contradiction by A2,A10,A15,Th12,TOPREAL1:25;
end;
assume i = j;
hence thesis by A1,A2,A3,A4,A5,A6,A9,Lm4;
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
being_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 that
A1: q1 in LSeg(f,i) and
A2: q2 in LSeg(f,i) and
A3: f is being_S-Seq and
A4: 1 <= i & i + 1 <= len f;
len f >= 2 by A3,TOPREAL1:def 8;
then reconsider
P = L~f, Q = LSeg(f,i) as non empty Subset of TOP-REAL 2 by A1,TOPREAL1:23;
L~f is_an_arc_of f/.1, f/.len f by A3,TOPREAL1:25;
then consider F being Function of I[01], (TOP-REAL 2)|P such that
A5: F is being_homeomorphism & F.0 = f/.1 & F.1 = f/.len f by TOPREAL1:def 1;
consider ppi, pi1 be Real such that
A6: ppi < pi1 and
A7: 0 <= ppi and
ppi <= 1 and
0 <= pi1 and
A8: pi1 <= 1 and
A9: LSeg (f, i) = F.:[.ppi, pi1.] and
A10: F.ppi = f/.i and
A11: F.pi1 = f/.(i+1) by A3,A4,A5,JORDAN5B:7;
set Ex = L[01]((#)(ppi,pi1),(ppi,pi1)(#));
A12: Ex is being_homeomorphism by A6,TREAL_1:17;
then
A13: rng Ex = [#] Closed-Interval-TSpace(ppi,pi1) by TOPS_2:def 5;
A14: ppi in { dd where dd is Real: ppi <= dd & dd <= pi1 } by A6;
then reconsider Poz = [.ppi,pi1.] as non empty Subset of I[01] by A7,A8,
BORSUK_1:40,RCOMP_1:def 1,XXREAL_1:34;
consider G be Function of I[01]|Poz, (TOP-REAL 2)|Q such that
A15: G = F|Poz and
A16: G is being_homeomorphism by A3,A4,A5,A9,JORDAN5B:8;
A17: ppi in [.ppi,pi1.] by A14,RCOMP_1:def 1;
set H = G * Ex;
A18: dom G = [#](I[01]|Poz) by A16,TOPS_2:def 5
.= Poz by PRE_TOPC:def 5
.= [#] Closed-Interval-TSpace(ppi,pi1) by A6,TOPMETR:18;
then
A19: rng H = rng G by A13,RELAT_1:28
.= [#] ((TOP-REAL 2)|LSeg(f,i)) by A16,TOPS_2:def 5;
pi1 in { dd where dd is Real: ppi <= dd & dd <= pi1 } by A6;
then
A20: pi1 in [.ppi,pi1.] by RCOMP_1:def 1;
A21: Ex.1 = Ex.(0,1)(#) by TREAL_1:def 2
.= (ppi,pi1)(#) by A6,TREAL_1:9
.= pi1 by A6,TREAL_1:def 2;
A22: dom H = dom Ex by A13,A18,RELAT_1:27
.= [#] I[01] by A12,TOPMETR:20,TOPS_2:def 5
.= the carrier of I[01];
then reconsider H as Function of I[01], (TOP-REAL 2)|Q by A19,FUNCT_2:2;
q1 in rng H by A1,A19,PRE_TOPC:def 5;
then consider x19 be object such that
A23: x19 in dom H and
A24: q1 = H.x19 by FUNCT_1:def 3;
x19 in { l where l is Real : 0 <= l & l <= 1 }
by A22,A23,BORSUK_1:40,RCOMP_1:def 1;
then consider x1 be Real such that
A25: x1 = x19 and
A26: 0 <= x1 & x1 <= 1;
assume
A27: LE q1, q2, L~f, f/.1, f/.len f;
x1 in the carrier of I[01] by A26,BORSUK_1:43;
then x1 in dom Ex by A13,A18,A22,RELAT_1:27;
then Ex.x1 in the carrier of Closed-Interval-TSpace(ppi,pi1) by A13,
FUNCT_1:def 3;
then
A28: Ex.x1 in Poz by A6,TOPMETR:18;
1 in dom H by A22,BORSUK_1:43;
then
A29: H.1 = G.pi1 by A21,FUNCT_1:12
.= f/.(i+1) by A11,A20,A15,FUNCT_1:49;
A30: Ex.0 = Ex.(#)(0,1) by TREAL_1:def 1
.= (#)(ppi,pi1) by A6,TREAL_1:9
.= ppi by A6,TREAL_1:def 1;
q2 in rng H by A2,A19,PRE_TOPC:def 5;
then consider x29 be object such that
A31: x29 in dom H and
A32: q2 = H.x29 by FUNCT_1:def 3;
x29 in { l where l is Real: 0 <= l & l <= 1 }
by A22,A31,BORSUK_1:40,RCOMP_1:def 1;
then consider x2 be Real such that
A33: x2 = x29 and
A34: 0 <= x2 and
A35: x2 <= 1;
reconsider X1 = x1, X2 = x2 as Point of Closed-Interval-TSpace (0,1) by A26
,A34,A35,BORSUK_1:43,TOPMETR:20;
x2 in the carrier of I[01] by A34,A35,BORSUK_1:43;
then x2 in dom Ex by A13,A18,A22,RELAT_1:27;
then Ex.x2 in the carrier of Closed-Interval-TSpace(ppi,pi1) by A13,
FUNCT_1:def 3;
then
A36: Ex.x2 in Poz by A6,TOPMETR:18;
then reconsider E1 = Ex.X1, E2 = Ex.X2 as Real by A28;
A37: q2 = G.(Ex.x2) by A31,A32,A33,FUNCT_1:12
.= F.(Ex.x2) by A15,A36,FUNCT_1:49;
reconsider K1 = Closed-Interval-TSpace(ppi,pi1), K2 = I[01]|Poz as SubSpace
of I[01] by A6,A7,A8,TOPMETR:20,TREAL_1:3;
A38: Ex is one-to-one continuous by A12,TOPS_2:def 5;
the carrier of K1 = [.ppi,pi1.] by A6,TOPMETR:18
.= [#](I[01]|Poz) by PRE_TOPC:def 5
.= the carrier of K2;
then I[01]|Poz = Closed-Interval-TSpace(ppi,pi1) by TSEP_1:5;
then
A39: H is being_homeomorphism by A16,A12,TOPMETR:20,TOPS_2:57;
A40: q1 = G.(Ex.x1) by A23,A24,A25,FUNCT_1:12
.= F.(Ex.x1) by A15,A28,FUNCT_1:49;
A41: 0 <= E2 & E2 <= 1 by A36,BORSUK_1:43;
0 in dom H by A22,BORSUK_1:43;
then
A42: H.0 = G.ppi by A30,FUNCT_1:12
.= f/.i by A10,A17,A15,FUNCT_1:49;
E1 <= 1 by A28,BORSUK_1:43;
then E1 <= E2 by A27,A5,A40,A37,A41;
then x1 <= x2 by A6,A30,A21,A38,JORDAN5A:15;
hence thesis by A3,A4,A39,A42,A29,A24,A32,A25,A26,A33,A35,Th8,JORDAN5B:15;
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 being_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 that
A1: q1 in L~f and
A2: q2 in L~f and
A3: f is being_S-Seq and
A4: q1 <> q2;
reconsider P = L~f as non empty Subset of TOP-REAL 2 by A1;
hereby
assume
A5: 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 that
A6: q1 in LSeg(f,i) and
A7: q2 in LSeg(f,j) and
A8: 1<=i and
A9: i+1<=len f and
A10: 1<=j & j+1<=len f;
thus i<=j
proof
assume j < i;
then j+1 <= i by NAT_1:13;
then consider m be Nat such that
A11: j+1+m = i by NAT_1:10;
A12: LE q2, f/.(j+1), P, p3, p4 by A3,A7,A10,Th26;
reconsider m as Nat;
A13: 1 <= j+1 & j+1 <= j+1+m by NAT_1:11;
i <= i + 1 by NAT_1:11;
then j+1+m <= len f by A9,A11,XXREAL_0:2;
then LE f/.(j+1), f/.(j+1+m), P, p3, p4 by A3,A13,Th24;
then
A14: LE q2, f/.(j+1+m), P, p3, p4 by A12,Th13;
LE f/.(j+1+m), q1, P, p3, p4 by A3,A6,A8,A9,A11,Th25;
then LE q2, q1, P, p3, p4 by A14,Th13;
hence thesis by A3,A4,A5,Th12,TOPREAL1:25;
end;
assume
A15: i = j;
A16: f is one-to-one by A3,TOPREAL1:def 8;
set p1 = f/.i, p2 = f/.(i+1);
A17: i in dom f & i+1 in dom f by A8,A9,SEQ_4:134;
A18: p1 <> p2
proof
assume p1 = p2;
then i = i+1 by A17,A16,PARTFUN2:10;
hence thesis;
end;
LSeg (f,i) = LSeg (p1, p2) by A8,A9,TOPREAL1:def 3;
hence thesis by A3,A5,A6,A7,A8,A9,A15,A18,Th17,Th29;
end;
end;
consider i be Nat such that
A19: 1 <= i & i+1 <= len f and
A20: q1 in LSeg(f,i) by A1,SPPOL_2:13;
consider j be Nat such that
A21: 1 <= j and
A22: j+1 <= len f and
A23: q2 in LSeg(f,j) by A2,SPPOL_2:13;
assume
A24: 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));
then
A25: i<=j by A19,A20,A21,A22,A23;
per cases by A25,XXREAL_0:1;
suppose
i < j;
then i+1 <= j by NAT_1:13;
then consider m be Nat such that
A26: j = i+1 + m by NAT_1:10;
reconsider m as Nat;
A27: 1 <= i+1 & i+1 <= i+1+m by NAT_1:11;
A28: LE q1, f/.(i+1), P, f/.1, f/.len f by A3,A19,A20,Th26;
j <= j + 1 by NAT_1:11;
then i+1+m <= len f by A22,A26,XXREAL_0:2;
then LE f/.(i+1), f/.(i+1+m), P, f/.1, f/.len f by A3,A27,Th24;
then
A29: LE q1, f/.(i+1+m), P, f/.1, f/.len f by A28,Th13;
LE f/.(i+1+m), q2, P, f/.1, f/.len f by A3,A21,A22,A23,A26,Th25;
hence thesis by A29,Th13;
end;
suppose
A30: i = j;
reconsider Q = LSeg (f,i) as non empty Subset of TOP-REAL 2 by A20;
set p1 = f/.i,p2 = f/.(i+1);
A31: f is one-to-one by A3,TOPREAL1:def 8;
A32: i in dom f & i+1 in dom f by A19,SEQ_4:134;
p1 <> p2
proof
assume p1 = p2;
then i = i+1 by A32,A31,PARTFUN2:10;
hence thesis;
end;
then consider
H be Function of I[01], (TOP-REAL 2) | LSeg(p1, p2) such that
A33: for x being Real st x in [.0,1.] holds H.x = (1-x)*p1 + x*p2 and
A34: H is being_homeomorphism and
H.0 = p1 and
H.1 = p2 by JORDAN5A:3;
A35: LSeg(f,i) = LSeg(p1,p2) by A19,TOPREAL1:def 3;
then reconsider H as Function of I[01], (TOP-REAL 2) | Q;
A36: LE q1, q2, f/.i, f/.(i+1) by A24,A19,A20,A23,A30;
q1 in P & q2 in P & for g being Function of I[01], (TOP-REAL 2)|P,
s1,s2 be Real
st g is being_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
A37: rng H = [#] ((TOP-REAL 2) | LSeg(f,i)) by A34,A35,TOPS_2:def 5
.= LSeg (f,i) by PRE_TOPC:def 5;
then consider x19 be object such that
A38: x19 in dom H and
A39: H.x19 = q1 by A20,FUNCT_1:def 3;
A40: dom H = [#]I[01] by A34,TOPS_2:def 5
.= [.0,1.] by BORSUK_1:40;
then x19 in { l where l is Real: 0 <= l & l <= 1 }
by A38,RCOMP_1:def 1;
then consider x1 be Real such that
A41: x1 = x19 and
0 <= x1 and
A42: x1 <= 1;
consider x29 be object such that
A43: x29 in dom H and
A44: H.x29 = q2 by A23,A30,A37,FUNCT_1:def 3;
x29 in { l where l is Real: 0 <= l & l <= 1 }
by A40,A43,RCOMP_1:def 1;
then consider x2 be Real such that
A45: x2 = x29 and
A46: 0 <= x2 & x2 <= 1;
A47: q2 = (1-x2)*p1 + x2*p2 by A33,A40,A43,A44,A45;
q1 = (1-x1)*p1 + x1*p2 by A33,A40,A38,A39,A41;
then
A48: x1 <= x2 by A36,A42,A46,A47;
0 in { l where l is Real: 0 <= l & l <= 1 };
then
A49: 0 in [.0,1.] by RCOMP_1:def 1;
then
A50: H.0 = (1-0)*p1 + 0 * p2 by A33
.= p1 + 0 * p2 by RLVECT_1:def 8
.= p1 + 0.TOP-REAL 2 by RLVECT_1:10
.= p1 by RLVECT_1:4;
thus q1 in P & q2 in P by A1,A2;
let F be Function of I[01], (TOP-REAL 2)|P, s1, s2 be Real;
assume that
A51: F is being_homeomorphism and
A52: F.0 = f/.1 & F.1 = f/.len f and
A53: F.s1 = q1 and
A54: 0 <= s1 & s1 <= 1 and
A55: F.s2 = q2 and
A56: 0 <= s2 & s2 <= 1;
consider ppi, pi1 be Real such that
A57: ppi < pi1 and
A58: 0 <= ppi and
ppi <= 1 and
0 <= pi1 and
A59: pi1 <= 1 and
A60: LSeg (f, i) = F.:[.ppi, pi1.] and
A61: F.ppi = f/.i and
A62: F.pi1 = f/.(i+1) by A3,A19,A51,A52,JORDAN5B:7;
A63: ppi in { dd where dd is Real: ppi <= dd & dd <= pi1 } by A57;
then reconsider
Poz = [.ppi,pi1.] as non empty Subset of I[01] by A58,A59,BORSUK_1:40
,RCOMP_1:def 1,XXREAL_1:34;
consider G be Function of I[01]|Poz, (TOP-REAL 2)|Q such that
A64: G = F|Poz and
A65: G is being_homeomorphism by A3,A19,A51,A52,A60,JORDAN5B:8;
A66: dom F = [#] I[01] by A51,TOPS_2:def 5
.= the carrier of I[01];
reconsider K1 = Closed-Interval-TSpace(ppi,pi1), K2 = I[01]|Poz as
SubSpace of I[01] by A57,A58,A59,TOPMETR:20,TREAL_1:3;
A67: the carrier of K1 = [.ppi,pi1.] by A57,TOPMETR:18
.= [#](I[01]|Poz) by PRE_TOPC:def 5
.= the carrier of K2;
then reconsider E=G" * H as Function of Closed-Interval-TSpace(0,1),
Closed-Interval-TSpace(ppi,pi1) by TOPMETR:20;
A68: G is one-to-one by A65,TOPS_2:def 5;
reconsider X1 = x1, X2 = x2 as Point of Closed-Interval-TSpace(0,1) by
A40,A38,A41,A43,A45,TOPMETR:18;
A69: G" is being_homeomorphism by A65,TOPS_2:56;
A70: s2 in the carrier of I[01] by A56,BORSUK_1:43;
A71: F is one-to-one by A51,TOPS_2:def 5;
rng G = [#] ((TOP-REAL 2)|LSeg(f,i)) by A65,TOPS_2:def 5;
then G is onto by FUNCT_2:def 3;
then
A72: G" = (G qua Function)" by A68,TOPS_2:def 4;
A73: ex x9 be object st x9 in dom F & x9 in [.ppi,pi1.] & q2 = F.x9
by A23,A30
,A60,FUNCT_1:def 6;
then s2 in Poz by A55,A70,A66,A71,FUNCT_1:def 4;
then
A74: G.s2 = q2 by A55,A64,FUNCT_1:49;
dom G = [#] (I[01]|Poz) by A65,TOPS_2:def 5;
then
A75: dom G = Poz by PRE_TOPC:def 5;
then s2 in dom G by A55,A70,A66,A71,A73,FUNCT_1:def 4;
then
A76: s2 = G".(H.x2) by A44,A45,A68,A72,A74,FUNCT_1:32
.= E.x2 by A43,A45,FUNCT_1:13;
then
A77: s2 = E.X2;
consider x be object such that
A78: x in dom F and
A79: x in [.ppi,pi1.] and
A80: q1 = F.x by A20,A60,FUNCT_1:def 6;
A81: s1 in the carrier of I[01] by A54,BORSUK_1:43;
then x = s1 by A53,A66,A71,A78,A80,FUNCT_1:def 4;
then
A82: G.s1 = q1 by A64,A79,A80,FUNCT_1:49;
Closed-Interval-TSpace(ppi,pi1) = I[01]|Poz by A67,TSEP_1:5;
then E is being_homeomorphism by A34,A35,A69,TOPMETR:20,TOPS_2:57;
then
A83: E is continuous one-to-one by TOPS_2:def 5;
1 in { l where l is Real: 0 <= l & l <= 1 };
then
A84: 1 in [.0,1.] by RCOMP_1:def 1;
then
A85: H.1 = (1-1)*p1 + 1*p2 by A33
.= 0.TOP-REAL 2 + 1*p2 by RLVECT_1:10
.= 0.TOP-REAL 2 + p2 by RLVECT_1:def 8
.= p2 by RLVECT_1:4;
s1 in dom G by A53,A81,A66,A71,A75,A79,A80,FUNCT_1:def 4;
then
A86: s1 = G".(H.x1) by A39,A41,A68,A72,A82,FUNCT_1:32
.= E.x1 by A38,A41,FUNCT_1:13;
then
A87: s1 = E.X1;
pi1 in { dd where dd is Real: ppi <= dd & dd <= pi1 } by A57;
then
A88: pi1 in [.ppi,pi1.] by RCOMP_1:def 1;
then G.pi1 = p2 by A62,A64,FUNCT_1:49;
then
A89: pi1 = G".(H.1) by A88,A68,A75,A72,A85,FUNCT_1:32
.= E.1 by A40,A84,FUNCT_1:13;
A90: ppi in [.ppi,pi1.] by A63,RCOMP_1:def 1;
then G.ppi = p1 by A61,A64,FUNCT_1:49;
then
A91: ppi = G".(H.0) by A90,A68,A75,A72,A50,FUNCT_1:32
.= E.0 by A40,A49,FUNCT_1:13;
per cases by A48,XXREAL_0:1;
suppose
x1 = x2;
hence thesis by A86,A76;
end;
suppose
x1 < x2;
hence thesis by A57,A83,A91,A89,A87,A77,JORDAN5A:15;
end;
end;
hence thesis;
end;
end;