let f be FinSequence of (TOP-REAL 2); :: thesis: for q1, q2 being Point of (TOP-REAL 2)

for 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 & LE q1,q2, L~ f,f /. 1,f /. (len f) holds

LE q1,q2, LSeg (f,i),f /. i,f /. (i + 1)

let q1, q2 be Point of (TOP-REAL 2); :: thesis: for 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 & LE q1,q2, L~ f,f /. 1,f /. (len f) holds

LE q1,q2, LSeg (f,i),f /. i,f /. (i + 1)

let i be Nat; :: thesis: ( q1 in LSeg (f,i) & q2 in LSeg (f,i) & f is being_S-Seq & 1 <= i & i + 1 <= len f & LE q1,q2, L~ f,f /. 1,f /. (len f) implies LE q1,q2, LSeg (f,i),f /. i,f /. (i + 1) )

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: ( not LE q1,q2, L~ f,f /. 1,f /. (len f) or LE q1,q2, LSeg (f,i),f /. i,f /. (i + 1) )

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: LE q1,q2, LSeg (f,i),f /. i,f /. (i + 1)

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: verum

for 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 & LE q1,q2, L~ f,f /. 1,f /. (len f) holds

LE q1,q2, LSeg (f,i),f /. i,f /. (i + 1)

let q1, q2 be Point of (TOP-REAL 2); :: thesis: for 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 & LE q1,q2, L~ f,f /. 1,f /. (len f) holds

LE q1,q2, LSeg (f,i),f /. i,f /. (i + 1)

let i be Nat; :: thesis: ( q1 in LSeg (f,i) & q2 in LSeg (f,i) & f is being_S-Seq & 1 <= i & i + 1 <= len f & LE q1,q2, L~ f,f /. 1,f /. (len f) implies LE q1,q2, LSeg (f,i),f /. i,f /. (i + 1) )

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: ( not LE q1,q2, L~ f,f /. 1,f /. (len f) or LE q1,q2, LSeg (f,i),f /. i,f /. (i + 1) )

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: LE q1,q2, LSeg (f,i),f /. i,f /. (i + 1)

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: verum