let f be FinSequence of (TOP-REAL 2); :: thesis: for 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) ) ) )

let q1, q2 be Point of (TOP-REAL 2); :: thesis: ( q1 in L~ f & q2 in L~ f & f is being_S-Seq & q1 <> q2 implies ( 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) ) ) ) )

set p3 = f /. 1;

set 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 ; :: thesis: ( 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) ) ) )

reconsider P = L~ f as non empty Subset of (TOP-REAL 2) by A1;

A19: ( 1 <= i & i + 1 <= len f ) and

A20: q1 in LSeg (f,i) by A1, SPPOL_2:13;

consider j being 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) ) ) ; :: thesis: LE q1,q2, L~ f,f /. 1,f /. (len f)

then A25: i <= j by A19, A20, A21, A22, A23;

( 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) ) ) )

let q1, q2 be Point of (TOP-REAL 2); :: thesis: ( q1 in L~ f & q2 in L~ f & f is being_S-Seq & q1 <> q2 implies ( 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) ) ) ) )

set p3 = f /. 1;

set 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 ; :: thesis: ( 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) ) ) )

reconsider P = L~ f as non empty Subset of (TOP-REAL 2) by A1;

hereby :: thesis: ( ( 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) ) ) ) implies LE q1,q2, L~ f,f /. 1,f /. (len f) )

consider i being Nat such that ( i <= j & ( i = j implies LE q1,q2,f /. i,f /. (i + 1) ) ) ) implies LE q1,q2, L~ f,f /. 1,f /. (len f) )

assume A5:
LE q1,q2, L~ f,f /. 1,f /. (len f)
; :: thesis: 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) ) )

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

end;( i <= j & ( i = j implies LE q1,q2,f /. i,f /. (i + 1) ) )

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

proof

let i, j be Nat; :: thesis: ( q1 in LSeg (f,i) & q2 in LSeg (f,j) & 1 <= i & i + 1 <= len f & 1 <= j & j + 1 <= len f implies ( i <= j & ( i = j implies LE q1,q2,f /. i,f /. (i + 1) ) ) )

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 ) ; :: thesis: ( i <= j & ( i = j implies LE q1,q2,f /. i,f /. (i + 1) ) )

thus i <= j :: thesis: ( i = j implies LE q1,q2,f /. i,f /. (i + 1) )

A16: f is one-to-one by A3, TOPREAL1:def 8;

set p1 = f /. i;

set p2 = f /. (i + 1);

A17: ( i in dom f & i + 1 in dom f ) by A8, A9, SEQ_4:134;

A18: f /. i <> f /. (i + 1)

hence LE q1,q2,f /. i,f /. (i + 1) by A3, A5, A6, A7, A8, A9, A15, A18, Th17, Th29; :: thesis: verum

end;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 ) ; :: thesis: ( i <= j & ( i = j implies LE q1,q2,f /. i,f /. (i + 1) ) )

thus i <= j :: thesis: ( i = j implies LE q1,q2,f /. i,f /. (i + 1) )

proof

assume A15:
i = j
; :: thesis: LE q1,q2,f /. i,f /. (i + 1)
assume
j < i
; :: thesis: contradiction

then j + 1 <= i by NAT_1:13;

then consider m being Nat such that

A11: (j + 1) + m = i by NAT_1:10;

A12: LE q2,f /. (j + 1),P,f /. 1,f /. (len f) by A3, A7, A10, Th26;

reconsider m = 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,f /. 1,f /. (len f) by A3, A13, Th24;

then A14: LE q2,f /. ((j + 1) + m),P,f /. 1,f /. (len f) by A12, Th13;

LE f /. ((j + 1) + m),q1,P,f /. 1,f /. (len f) by A3, A6, A8, A9, A11, Th25;

then LE q2,q1,P,f /. 1,f /. (len f) by A14, Th13;

hence contradiction by A3, A4, A5, Th12, TOPREAL1:25; :: thesis: verum

end;then j + 1 <= i by NAT_1:13;

then consider m being Nat such that

A11: (j + 1) + m = i by NAT_1:10;

A12: LE q2,f /. (j + 1),P,f /. 1,f /. (len f) by A3, A7, A10, Th26;

reconsider m = 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,f /. 1,f /. (len f) by A3, A13, Th24;

then A14: LE q2,f /. ((j + 1) + m),P,f /. 1,f /. (len f) by A12, Th13;

LE f /. ((j + 1) + m),q1,P,f /. 1,f /. (len f) by A3, A6, A8, A9, A11, Th25;

then LE q2,q1,P,f /. 1,f /. (len f) by A14, Th13;

hence contradiction by A3, A4, A5, Th12, TOPREAL1:25; :: thesis: verum

A16: f is one-to-one by A3, TOPREAL1:def 8;

set p1 = f /. i;

set p2 = f /. (i + 1);

A17: ( i in dom f & i + 1 in dom f ) by A8, A9, SEQ_4:134;

A18: f /. i <> f /. (i + 1)

proof

LSeg (f,i) = LSeg ((f /. i),(f /. (i + 1)))
by A8, A9, TOPREAL1:def 3;
assume
f /. i = f /. (i + 1)
; :: thesis: contradiction

then i = i + 1 by A17, A16, PARTFUN2:10;

hence contradiction ; :: thesis: verum

end;then i = i + 1 by A17, A16, PARTFUN2:10;

hence contradiction ; :: thesis: verum

hence LE q1,q2,f /. i,f /. (i + 1) by A3, A5, A6, A7, A8, A9, A15, A18, Th17, Th29; :: thesis: verum

A19: ( 1 <= i & i + 1 <= len f ) and

A20: q1 in LSeg (f,i) by A1, SPPOL_2:13;

consider j being 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) ) ) ; :: thesis: LE q1,q2, L~ f,f /. 1,f /. (len f)

then A25: i <= j by A19, A20, A21, A22, A23;

per cases
( i < j or i = j )
by A25, XXREAL_0:1;

end;

suppose
i < j
; :: thesis: LE q1,q2, L~ f,f /. 1,f /. (len f)

then
i + 1 <= j
by NAT_1:13;

then consider m being Nat such that

A26: j = (i + 1) + m by NAT_1:10;

reconsider m = 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 LE q1,q2, L~ f,f /. 1,f /. (len f) by A29, Th13; :: thesis: verum

end;then consider m being Nat such that

A26: j = (i + 1) + m by NAT_1:10;

reconsider m = 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 LE q1,q2, L~ f,f /. 1,f /. (len f) by A29, Th13; :: thesis: verum

suppose A30:
i = j
; :: thesis: LE q1,q2, L~ f,f /. 1,f /. (len f)

reconsider Q = LSeg (f,i) as non empty Subset of (TOP-REAL 2) by A20;

set p1 = f /. i;

set 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;

f /. i <> f /. (i + 1)

A33: for x being Real st x in [.0,1.] holds

H . x = ((1 - x) * (f /. i)) + (x * (f /. (i + 1))) and

A34: H is being_homeomorphism and

H . 0 = f /. i and

H . 1 = f /. (i + 1) by JORDAN5A:3;

A35: LSeg (f,i) = LSeg ((f /. i),(f /. (i + 1))) by A19, TOPREAL1:def 3;

then reconsider H = 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)

for 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 = q2 & 0 <= s2 & s2 <= 1 holds

s1 <= s2 ) )

end;set p1 = f /. i;

set 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;

f /. i <> f /. (i + 1)

proof

then consider H being Function of I[01],((TOP-REAL 2) | (LSeg ((f /. i),(f /. (i + 1))))) such that
assume
f /. i = f /. (i + 1)
; :: thesis: contradiction

then i = i + 1 by A32, A31, PARTFUN2:10;

hence contradiction ; :: thesis: verum

end;then i = i + 1 by A32, A31, PARTFUN2:10;

hence contradiction ; :: thesis: verum

A33: for x being Real st x in [.0,1.] holds

H . x = ((1 - x) * (f /. i)) + (x * (f /. (i + 1))) and

A34: H is being_homeomorphism and

H . 0 = f /. i and

H . 1 = f /. (i + 1) by JORDAN5A:3;

A35: LSeg (f,i) = LSeg ((f /. i),(f /. (i + 1))) by A19, TOPREAL1:def 3;

then reconsider H = 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)

for 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 = q2 & 0 <= s2 & s2 <= 1 holds

s1 <= s2 ) )

proof

hence
LE q1,q2, L~ f,f /. 1,f /. (len f)
; :: thesis: verum
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 being 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 being Real such that

A41: x1 = x19 and

0 <= x1 and

A42: x1 <= 1 ;

consider x29 being 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 being Real such that

A45: x2 = x29 and

A46: ( 0 <= x2 & x2 <= 1 ) ;

A47: q2 = ((1 - x2) * (f /. i)) + (x2 * (f /. (i + 1))) by A33, A40, A43, A44, A45;

q1 = ((1 - x1) * (f /. i)) + (x1 * (f /. (i + 1))) 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) * (f /. i)) + (0 * (f /. (i + 1))) by A33

.= (f /. i) + (0 * (f /. (i + 1))) by RLVECT_1:def 8

.= (f /. i) + (0. (TOP-REAL 2)) by RLVECT_1:10

.= f /. i by RLVECT_1:4 ;

thus ( q1 in P & q2 in P ) by A1, A2; :: thesis: for g being Function of I[01],((TOP-REAL 2) | P)

for 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 = q2 & 0 <= s2 & s2 <= 1 holds

s1 <= s2

let F be Function of I[01],((TOP-REAL 2) | P); :: thesis: for s1, s2 being Real st F is being_homeomorphism & F . 0 = f /. 1 & F . 1 = f /. (len f) & F . s1 = q1 & 0 <= s1 & s1 <= 1 & F . s2 = q2 & 0 <= s2 & s2 <= 1 holds

s1 <= s2

let s1, s2 be Real; :: thesis: ( F is being_homeomorphism & F . 0 = f /. 1 & F . 1 = f /. (len f) & F . s1 = q1 & 0 <= s1 & s1 <= 1 & F . s2 = q2 & 0 <= s2 & s2 <= 1 implies s1 <= s2 )

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 ) ; :: thesis: s1 <= s2

consider ppi, pi1 being 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 being 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 " by A68, TOPS_2:def 4;

A73: ex x9 being 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 being 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 & E is 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) * (f /. i)) + (1 * (f /. (i + 1))) by A33

.= (0. (TOP-REAL 2)) + (1 * (f /. (i + 1))) by RLVECT_1:10

.= (0. (TOP-REAL 2)) + (f /. (i + 1)) by RLVECT_1:def 8

.= f /. (i + 1) 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 = f /. (i + 1) 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 = f /. i 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 ;

end;.= LSeg (f,i) by PRE_TOPC:def 5 ;

then consider x19 being 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 being Real such that

A41: x1 = x19 and

0 <= x1 and

A42: x1 <= 1 ;

consider x29 being 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 being Real such that

A45: x2 = x29 and

A46: ( 0 <= x2 & x2 <= 1 ) ;

A47: q2 = ((1 - x2) * (f /. i)) + (x2 * (f /. (i + 1))) by A33, A40, A43, A44, A45;

q1 = ((1 - x1) * (f /. i)) + (x1 * (f /. (i + 1))) 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) * (f /. i)) + (0 * (f /. (i + 1))) by A33

.= (f /. i) + (0 * (f /. (i + 1))) by RLVECT_1:def 8

.= (f /. i) + (0. (TOP-REAL 2)) by RLVECT_1:10

.= f /. i by RLVECT_1:4 ;

thus ( q1 in P & q2 in P ) by A1, A2; :: thesis: for g being Function of I[01],((TOP-REAL 2) | P)

for 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 = q2 & 0 <= s2 & s2 <= 1 holds

s1 <= s2

let F be Function of I[01],((TOP-REAL 2) | P); :: thesis: for s1, s2 being Real st F is being_homeomorphism & F . 0 = f /. 1 & F . 1 = f /. (len f) & F . s1 = q1 & 0 <= s1 & s1 <= 1 & F . s2 = q2 & 0 <= s2 & s2 <= 1 holds

s1 <= s2

let s1, s2 be Real; :: thesis: ( F is being_homeomorphism & F . 0 = f /. 1 & F . 1 = f /. (len f) & F . s1 = q1 & 0 <= s1 & s1 <= 1 & F . s2 = q2 & 0 <= s2 & s2 <= 1 implies s1 <= s2 )

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 ) ; :: thesis: s1 <= s2

consider ppi, pi1 being 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 being 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 " by A68, TOPS_2:def 4;

A73: ex x9 being 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 being 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 & E is 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) * (f /. i)) + (1 * (f /. (i + 1))) by A33

.= (0. (TOP-REAL 2)) + (1 * (f /. (i + 1))) by RLVECT_1:10

.= (0. (TOP-REAL 2)) + (f /. (i + 1)) by RLVECT_1:def 8

.= f /. (i + 1) 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 = f /. (i + 1) 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 = f /. i 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 ;