let f be FinSequence of (TOP-REAL 2); :: thesis:
let q1, q2 be Point of (TOP-REAL 2); :: thesis:
let i be Nat; :: thesis:
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 ) ; :: thesis:
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 being 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: L[01] (((#) (ppi,pi1)),((ppi,pi1) (#))) is being_homeomorphism by A6, TREAL_1:17;
then A13: rng (L[01] (((#) (ppi,pi1)),((ppi,pi1) (#)))) = [#] (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 being 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 * (L[01] (((#) (ppi,pi1)),((ppi,pi1) (#))));
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 (G * (L[01] (((#) (ppi,pi1)),((ppi,pi1) (#))))) = 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: (L[01] (((#) (ppi,pi1)),((ppi,pi1) (#)))) . 1 = (L[01] (((#) (ppi,pi1)),((ppi,pi1) (#)))) . ((0,1) (#)) by TREAL_1:def 2
.= (ppi,pi1) (#) by A6, TREAL_1:9
.= pi1 by A6, TREAL_1:def 2 ;
A22: dom (G * (L[01] (((#) (ppi,pi1)),((ppi,pi1) (#))))) = dom (L[01] (((#) (ppi,pi1)),((ppi,pi1) (#)))) by A13, A18, RELAT_1:27
.= [#] I[01] by A12, TOPMETR:20, TOPS_2:def 5
.= the carrier of I[01] ;
then reconsider H = G * (L[01] (((#) (ppi,pi1)),((ppi,pi1) (#)))) 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 being 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 being Real such that
A25: x1 = x19 and
A26: ( 0 <= x1 & x1 <= 1 ) ;
assume A27: LE q1,q2, L~ f,f /. 1,f /. (len f) ; :: thesis:
x1 in the carrier of I[01] by A26, BORSUK_1:43;
then x1 in dom (L[01] (((#) (ppi,pi1)),((ppi,pi1) (#)))) by A13, A18, A22, RELAT_1:27;
then (L[01] (((#) (ppi,pi1)),((ppi,pi1) (#)))) . x1 in the carrier of (Closed-Interval-TSpace (ppi,pi1)) by A13, FUNCT_1:def 3;
then A28: (L[01] (((#) (ppi,pi1)),((ppi,pi1) (#)))) . 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: (L[01] (((#) (ppi,pi1)),((ppi,pi1) (#)))) . 0 = (L[01] (((#) (ppi,pi1)),((ppi,pi1) (#)))) . ((#) (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 being 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 being 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 (L[01] (((#) (ppi,pi1)),((ppi,pi1) (#)))) by A13, A18, A22, RELAT_1:27;
then (L[01] (((#) (ppi,pi1)),((ppi,pi1) (#)))) . x2 in the carrier of (Closed-Interval-TSpace (ppi,pi1)) by A13, FUNCT_1:def 3;
then A36: (L[01] (((#) (ppi,pi1)),((ppi,pi1) (#)))) . x2 in Poz by A6, TOPMETR:18;
then reconsider E1 = (L[01] (((#) (ppi,pi1)),((ppi,pi1) (#)))) . X1, E2 = (L[01] (((#) (ppi,pi1)),((ppi,pi1) (#)))) . X2 as Real by A28;
A37: q2 = G . ((L[01] (((#) (ppi,pi1)),((ppi,pi1) (#)))) . x2) by A31, A32, A33, FUNCT_1:12
.= F . ((L[01] (((#) (ppi,pi1)),((ppi,pi1) (#)))) . 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: ( L[01] (((#) (ppi,pi1)),((ppi,pi1) (#))) is one-to-one & L[01] (((#) (ppi,pi1)),((ppi,pi1) (#))) is 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 . ((L[01] (((#) (ppi,pi1)),((ppi,pi1) (#)))) . x1) by A23, A24, A25, FUNCT_1:12
.= F . ((L[01] (((#) (ppi,pi1)),((ppi,pi1) (#)))) . 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 LE q1,q2, LSeg (f,i),f /. i,f /. (i + 1) by A3, A4, A39, A42, A29, A24, A32, A25, A26, A33, A35, Th8, JORDAN5B:15; :: thesis: