let f be FinSequence of (TOP-REAL 2); :: thesis: for a, c, d being Real st 1 <= len f & X_axis f lies_between (X_axis f) . 1,(X_axis f) . (len f) & Y_axis f lies_between c,d & a > 0 & ( for i being Nat st 1 <= i & i + 1 <= len f holds

|.((f /. i) - (f /. (i + 1))).| < a ) holds

ex g being FinSequence of (TOP-REAL 2) st

( g is special & g . 1 = f . 1 & g . (len g) = f . (len f) & len g >= len f & X_axis g lies_between (X_axis f) . 1,(X_axis f) . (len f) & Y_axis g lies_between c,d & ( for j being Nat st j in dom g holds

ex k being Nat st

( k in dom f & |.((g /. j) - (f /. k)).| < a ) ) & ( for j being Nat st 1 <= j & j + 1 <= len g holds

|.((g /. j) - (g /. (j + 1))).| < a ) )

let a, c, d be Real; :: thesis: ( 1 <= len f & X_axis f lies_between (X_axis f) . 1,(X_axis f) . (len f) & Y_axis f lies_between c,d & a > 0 & ( for i being Nat st 1 <= i & i + 1 <= len f holds

|.((f /. i) - (f /. (i + 1))).| < a ) implies ex g being FinSequence of (TOP-REAL 2) st

( g is special & g . 1 = f . 1 & g . (len g) = f . (len f) & len g >= len f & X_axis g lies_between (X_axis f) . 1,(X_axis f) . (len f) & Y_axis g lies_between c,d & ( for j being Nat st j in dom g holds

ex k being Nat st

( k in dom f & |.((g /. j) - (f /. k)).| < a ) ) & ( for j being Nat st 1 <= j & j + 1 <= len g holds

|.((g /. j) - (g /. (j + 1))).| < a ) ) )

assume that

A1: 1 <= len f and

A2: X_axis f lies_between (X_axis f) . 1,(X_axis f) . (len f) and

A3: Y_axis f lies_between c,d and

A4: a > 0 and

A5: for i being Nat st 1 <= i & i + 1 <= len f holds

|.((f /. i) - (f /. (i + 1))).| < a ; :: thesis: ex g being FinSequence of (TOP-REAL 2) st

( g is special & g . 1 = f . 1 & g . (len g) = f . (len f) & len g >= len f & X_axis g lies_between (X_axis f) . 1,(X_axis f) . (len f) & Y_axis g lies_between c,d & ( for j being Nat st j in dom g holds

ex k being Nat st

( k in dom f & |.((g /. j) - (f /. k)).| < a ) ) & ( for j being Nat st 1 <= j & j + 1 <= len g holds

|.((g /. j) - (g /. (j + 1))).| < a ) )

A6: f . (len f) = f /. (len f) by A1, FINSEQ_4:15;

defpred S_{1}[ set , object ] means for j being Nat st ( $1 = 2 * j or $1 = (2 * j) -' 1 ) holds

( ( $1 = 2 * j implies $2 = |[((f /. j) `1),((f /. (j + 1)) `2)]| ) & ( $1 = (2 * j) -' 1 implies $2 = f /. j ) );

A7: for k being Nat st k in Seg ((2 * (len f)) -' 1) holds

ex x being object st S_{1}[k,x]

( dom p = Seg ((2 * (len f)) -' 1) & ( for k being Nat st k in Seg ((2 * (len f)) -' 1) holds

S_{1}[k,p . k] ) )
from FINSEQ_1:sch 1(A7);

then consider p being FinSequence such that

A24: dom p = Seg ((2 * (len f)) -' 1) and

A25: for k being Nat st k in Seg ((2 * (len f)) -' 1) holds

for j being Nat st ( k = 2 * j or k = (2 * j) -' 1 ) holds

( ( k = 2 * j implies p . k = |[((f /. j) `1),((f /. (j + 1)) `2)]| ) & ( k = (2 * j) -' 1 implies p . k = f /. j ) ) ;

rng p c= the carrier of (TOP-REAL 2)

A33: len p = (2 * (len f)) -' 1 by A24, FINSEQ_1:def 3;

for i being Nat st 1 <= i & i + 1 <= len g1 & not (g1 /. i) `1 = (g1 /. (i + 1)) `1 holds

(g1 /. i) `2 = (g1 /. (i + 1)) `2

A49: 2 * (len f) >= 2 * 1 by A1, XREAL_1:64;

then A50: (2 * (len f)) -' 1 = (2 * (len f)) - 1 by XREAL_1:233, XXREAL_0:2;

for i being Nat st i in dom (Y_axis g1) holds

( c <= (Y_axis g1) . i & (Y_axis g1) . i <= d )

for i being Nat st i in dom (X_axis g1) holds

( (X_axis f) . 1 <= (X_axis g1) . i & (X_axis g1) . i <= (X_axis f) . (len f) )

(len f) + (len f) >= (len f) + 1 by A1, XREAL_1:6;

then A86: (2 * (len f)) - 1 >= ((len f) + 1) - 1 by XREAL_1:9;

A87: (2 * 1) -' 1 = (1 + 1) -' 1

.= 1 by NAT_D:34 ;

A88: (2 * (len f)) - 1 >= (1 + 1) - 1 by A49, XREAL_1:9;

then 1 in Seg ((2 * (len f)) -' 1) by A50, FINSEQ_1:1;

then A89: p . 1 = f /. 1 by A25, A87;

A90: for i being Nat st 1 <= i & i + 1 <= len g1 holds

|.((g1 /. i) - (g1 /. (i + 1))).| < a

ex k being Nat st

( k in dom f & |.((g1 /. i) - (f /. k)).| < a )

then g1 . (len g1) = f . (len f) by A25, A33, A6;

hence ex g being FinSequence of (TOP-REAL 2) st

( g is special & g . 1 = f . 1 & g . (len g) = f . (len f) & len g >= len f & X_axis g lies_between (X_axis f) . 1,(X_axis f) . (len f) & Y_axis g lies_between c,d & ( for j being Nat st j in dom g holds

ex k being Nat st

( k in dom f & |.((g /. j) - (f /. k)).| < a ) ) & ( for j being Nat st 1 <= j & j + 1 <= len g holds

|.((g /. j) - (g /. (j + 1))).| < a ) ) by A1, A33, A48, A50, A89, A86, A85, A67, A114, A90, FINSEQ_4:15; :: thesis: verum

|.((f /. i) - (f /. (i + 1))).| < a ) holds

ex g being FinSequence of (TOP-REAL 2) st

( g is special & g . 1 = f . 1 & g . (len g) = f . (len f) & len g >= len f & X_axis g lies_between (X_axis f) . 1,(X_axis f) . (len f) & Y_axis g lies_between c,d & ( for j being Nat st j in dom g holds

ex k being Nat st

( k in dom f & |.((g /. j) - (f /. k)).| < a ) ) & ( for j being Nat st 1 <= j & j + 1 <= len g holds

|.((g /. j) - (g /. (j + 1))).| < a ) )

let a, c, d be Real; :: thesis: ( 1 <= len f & X_axis f lies_between (X_axis f) . 1,(X_axis f) . (len f) & Y_axis f lies_between c,d & a > 0 & ( for i being Nat st 1 <= i & i + 1 <= len f holds

|.((f /. i) - (f /. (i + 1))).| < a ) implies ex g being FinSequence of (TOP-REAL 2) st

( g is special & g . 1 = f . 1 & g . (len g) = f . (len f) & len g >= len f & X_axis g lies_between (X_axis f) . 1,(X_axis f) . (len f) & Y_axis g lies_between c,d & ( for j being Nat st j in dom g holds

ex k being Nat st

( k in dom f & |.((g /. j) - (f /. k)).| < a ) ) & ( for j being Nat st 1 <= j & j + 1 <= len g holds

|.((g /. j) - (g /. (j + 1))).| < a ) ) )

assume that

A1: 1 <= len f and

A2: X_axis f lies_between (X_axis f) . 1,(X_axis f) . (len f) and

A3: Y_axis f lies_between c,d and

A4: a > 0 and

A5: for i being Nat st 1 <= i & i + 1 <= len f holds

|.((f /. i) - (f /. (i + 1))).| < a ; :: thesis: ex g being FinSequence of (TOP-REAL 2) st

( g is special & g . 1 = f . 1 & g . (len g) = f . (len f) & len g >= len f & X_axis g lies_between (X_axis f) . 1,(X_axis f) . (len f) & Y_axis g lies_between c,d & ( for j being Nat st j in dom g holds

ex k being Nat st

( k in dom f & |.((g /. j) - (f /. k)).| < a ) ) & ( for j being Nat st 1 <= j & j + 1 <= len g holds

|.((g /. j) - (g /. (j + 1))).| < a ) )

A6: f . (len f) = f /. (len f) by A1, FINSEQ_4:15;

defpred S

( ( $1 = 2 * j implies $2 = |[((f /. j) `1),((f /. (j + 1)) `2)]| ) & ( $1 = (2 * j) -' 1 implies $2 = f /. j ) );

A7: for k being Nat st k in Seg ((2 * (len f)) -' 1) holds

ex x being object st S

proof

ex p being FinSequence st
let k be Nat; :: thesis: ( k in Seg ((2 * (len f)) -' 1) implies ex x being object st S_{1}[k,x] )

assume A8: k in Seg ((2 * (len f)) -' 1) ; :: thesis: ex x being object st S_{1}[k,x]

then A9: 1 <= k by FINSEQ_1:1;

end;assume A8: k in Seg ((2 * (len f)) -' 1) ; :: thesis: ex x being object st S

then A9: 1 <= k by FINSEQ_1:1;

per cases
( k mod 2 = 0 or k mod 2 = 1 )
by NAT_D:12;

end;

suppose A10:
k mod 2 = 0
; :: thesis: ex x being object st S_{1}[k,x]

consider i being Nat such that

A11: k = (2 * i) + (k mod 2) and

k mod 2 < 2 by NAT_D:def 2;

for j being Nat st ( k = 2 * j or k = (2 * j) -' 1 ) holds

( ( k = 2 * j implies |[((f /. i) `1),((f /. (i + 1)) `2)]| = |[((f /. j) `1),((f /. (j + 1)) `2)]| ) & ( k = (2 * j) -' 1 implies |[((f /. i) `1),((f /. (i + 1)) `2)]| = f /. j ) )_{1}[k,x]
; :: thesis: verum

end;A11: k = (2 * i) + (k mod 2) and

k mod 2 < 2 by NAT_D:def 2;

for j being Nat st ( k = 2 * j or k = (2 * j) -' 1 ) holds

( ( k = 2 * j implies |[((f /. i) `1),((f /. (i + 1)) `2)]| = |[((f /. j) `1),((f /. (j + 1)) `2)]| ) & ( k = (2 * j) -' 1 implies |[((f /. i) `1),((f /. (i + 1)) `2)]| = f /. j ) )

proof

hence
ex x being object st S
let j be Nat; :: thesis: ( ( k = 2 * j or k = (2 * j) -' 1 ) implies ( ( k = 2 * j implies |[((f /. i) `1),((f /. (i + 1)) `2)]| = |[((f /. j) `1),((f /. (j + 1)) `2)]| ) & ( k = (2 * j) -' 1 implies |[((f /. i) `1),((f /. (i + 1)) `2)]| = f /. j ) ) )

assume ( k = 2 * j or k = (2 * j) -' 1 ) ; :: thesis: ( ( k = 2 * j implies |[((f /. i) `1),((f /. (i + 1)) `2)]| = |[((f /. j) `1),((f /. (j + 1)) `2)]| ) & ( k = (2 * j) -' 1 implies |[((f /. i) `1),((f /. (i + 1)) `2)]| = f /. j ) )

end;assume ( k = 2 * j or k = (2 * j) -' 1 ) ; :: thesis: ( ( k = 2 * j implies |[((f /. i) `1),((f /. (i + 1)) `2)]| = |[((f /. j) `1),((f /. (j + 1)) `2)]| ) & ( k = (2 * j) -' 1 implies |[((f /. i) `1),((f /. (i + 1)) `2)]| = f /. j ) )

now :: thesis: not k = (2 * j) -' 1

hence
( ( k = 2 * j implies |[((f /. i) `1),((f /. (i + 1)) `2)]| = |[((f /. j) `1),((f /. (j + 1)) `2)]| ) & ( k = (2 * j) -' 1 implies |[((f /. i) `1),((f /. (i + 1)) `2)]| = f /. j ) )
by A10, A11; :: thesis: verumassume A12:
k = (2 * j) -' 1
; :: thesis: contradiction

k = ((2 * (j - 1)) + (1 + 1)) - 1 by A9, A12, NAT_D:39

.= (2 * (j - 1)) + 1 ;

then k = (2 * (j -' 1)) + 1 by A14, XREAL_1:233;

hence contradiction by A10, NAT_D:def 2; :: thesis: verum

end;now :: thesis: not j = 0

then A14:
j >= 0 + 1
by NAT_1:13;
0 - 1 < 0
;

then A13: 0 -' 1 = 0 by XREAL_0:def 2;

assume j = 0 ; :: thesis: contradiction

hence contradiction by A8, A12, A13, FINSEQ_1:1; :: thesis: verum

end;then A13: 0 -' 1 = 0 by XREAL_0:def 2;

assume j = 0 ; :: thesis: contradiction

hence contradiction by A8, A12, A13, FINSEQ_1:1; :: thesis: verum

k = ((2 * (j - 1)) + (1 + 1)) - 1 by A9, A12, NAT_D:39

.= (2 * (j - 1)) + 1 ;

then k = (2 * (j -' 1)) + 1 by A14, XREAL_1:233;

hence contradiction by A10, NAT_D:def 2; :: thesis: verum

suppose A15:
k mod 2 = 1
; :: thesis: ex x being object st S_{1}[k,x]

consider i being Nat such that

A16: k = (2 * i) + (k mod 2) and

A17: k mod 2 < 2 by NAT_D:def 2;

for j being Nat st ( k = 2 * j or k = (2 * j) -' 1 ) holds

( ( k = 2 * j implies f /. (i + 1) = |[((f /. j) `1),((f /. (j + 1)) `2)]| ) & ( k = (2 * j) -' 1 implies f /. (i + 1) = f /. j ) )_{1}[k,x]
; :: thesis: verum

end;A16: k = (2 * i) + (k mod 2) and

A17: k mod 2 < 2 by NAT_D:def 2;

for j being Nat st ( k = 2 * j or k = (2 * j) -' 1 ) holds

( ( k = 2 * j implies f /. (i + 1) = |[((f /. j) `1),((f /. (j + 1)) `2)]| ) & ( k = (2 * j) -' 1 implies f /. (i + 1) = f /. j ) )

proof

hence
ex x being object st S
let j be Nat; :: thesis: ( ( k = 2 * j or k = (2 * j) -' 1 ) implies ( ( k = 2 * j implies f /. (i + 1) = |[((f /. j) `1),((f /. (j + 1)) `2)]| ) & ( k = (2 * j) -' 1 implies f /. (i + 1) = f /. j ) ) )

assume A18: ( k = 2 * j or k = (2 * j) -' 1 ) ; :: thesis: ( ( k = 2 * j implies f /. (i + 1) = |[((f /. j) `1),((f /. (j + 1)) `2)]| ) & ( k = (2 * j) -' 1 implies f /. (i + 1) = f /. j ) )

end;assume A18: ( k = 2 * j or k = (2 * j) -' 1 ) ; :: thesis: ( ( k = 2 * j implies f /. (i + 1) = |[((f /. j) `1),((f /. (j + 1)) `2)]| ) & ( k = (2 * j) -' 1 implies f /. (i + 1) = f /. j ) )

per cases
( k = (2 * j) -' 1 or k = 2 * j )
by A18;

end;

suppose A19:
k = (2 * j) -' 1
; :: thesis: ( ( k = 2 * j implies f /. (i + 1) = |[((f /. j) `1),((f /. (j + 1)) `2)]| ) & ( k = (2 * j) -' 1 implies f /. (i + 1) = f /. j ) )

hence ( ( k = 2 * j implies f /. (i + 1) = |[((f /. j) `1),((f /. (j + 1)) `2)]| ) & ( k = (2 * j) -' 1 implies f /. (i + 1) = f /. j ) ) by A20; :: thesis: verum

end;

A20: now :: thesis: ( k = (2 * j) -' 1 implies f /. (i + 1) = f /. j )

k = (2 * j) - 1
by A9, A19, NAT_D:39;assume
k = (2 * j) -' 1
; :: thesis: f /. (i + 1) = f /. j

then k = ((2 * (j - 1)) + (1 + 1)) - 1 by A9, NAT_D:39

.= (2 * (j - 1)) + 1 ;

hence f /. (i + 1) = f /. j by A15, A16; :: thesis: verum

end;then k = ((2 * (j - 1)) + (1 + 1)) - 1 by A9, NAT_D:39

.= (2 * (j - 1)) + 1 ;

hence f /. (i + 1) = f /. j by A15, A16; :: thesis: verum

hence ( ( k = 2 * j implies f /. (i + 1) = |[((f /. j) `1),((f /. (j + 1)) `2)]| ) & ( k = (2 * j) -' 1 implies f /. (i + 1) = f /. j ) ) by A20; :: thesis: verum

suppose A21:
k = 2 * j
; :: thesis: ( ( k = 2 * j implies f /. (i + 1) = |[((f /. j) `1),((f /. (j + 1)) `2)]| ) & ( k = (2 * j) -' 1 implies f /. (i + 1) = f /. j ) )

then A22:
2 * (j - i) = 1
by A15, A16;

then j - i >= 0 ;

then A23: j - i = j -' i by XREAL_0:def 2;

( j - i = 0 or j - i > 0 ) by A22;

then j - i >= 0 + 1 by A15, A16, A21, A23, NAT_1:13;

then 2 * (j - i) >= 2 * 1 by XREAL_1:64;

hence ( ( k = 2 * j implies f /. (i + 1) = |[((f /. j) `1),((f /. (j + 1)) `2)]| ) & ( k = (2 * j) -' 1 implies f /. (i + 1) = f /. j ) ) by A16, A17, A21; :: thesis: verum

end;then j - i >= 0 ;

then A23: j - i = j -' i by XREAL_0:def 2;

( j - i = 0 or j - i > 0 ) by A22;

then j - i >= 0 + 1 by A15, A16, A21, A23, NAT_1:13;

then 2 * (j - i) >= 2 * 1 by XREAL_1:64;

hence ( ( k = 2 * j implies f /. (i + 1) = |[((f /. j) `1),((f /. (j + 1)) `2)]| ) & ( k = (2 * j) -' 1 implies f /. (i + 1) = f /. j ) ) by A16, A17, A21; :: thesis: verum

( dom p = Seg ((2 * (len f)) -' 1) & ( for k being Nat st k in Seg ((2 * (len f)) -' 1) holds

S

then consider p being FinSequence such that

A24: dom p = Seg ((2 * (len f)) -' 1) and

A25: for k being Nat st k in Seg ((2 * (len f)) -' 1) holds

for j being Nat st ( k = 2 * j or k = (2 * j) -' 1 ) holds

( ( k = 2 * j implies p . k = |[((f /. j) `1),((f /. (j + 1)) `2)]| ) & ( k = (2 * j) -' 1 implies p . k = f /. j ) ) ;

rng p c= the carrier of (TOP-REAL 2)

proof

then reconsider g1 = p as FinSequence of (TOP-REAL 2) by FINSEQ_1:def 4;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng p or y in the carrier of (TOP-REAL 2) )

assume y in rng p ; :: thesis: y in the carrier of (TOP-REAL 2)

then consider x being object such that

A26: x in dom p and

A27: y = p . x by FUNCT_1:def 3;

reconsider i = x as Element of NAT by A26;

x in Seg (len p) by A26, FINSEQ_1:def 3;

then A28: 1 <= i by FINSEQ_1:1;

end;assume y in rng p ; :: thesis: y in the carrier of (TOP-REAL 2)

then consider x being object such that

A26: x in dom p and

A27: y = p . x by FUNCT_1:def 3;

reconsider i = x as Element of NAT by A26;

x in Seg (len p) by A26, FINSEQ_1:def 3;

then A28: 1 <= i by FINSEQ_1:1;

per cases
( i mod 2 = 0 or i mod 2 = 1 )
by NAT_D:12;

end;

suppose A29:
i mod 2 = 0
; :: thesis: y in the carrier of (TOP-REAL 2)

consider j being Nat such that

A30: i = (2 * j) + (i mod 2) and

i mod 2 < 2 by NAT_D:def 2;

reconsider j = j as Element of NAT by ORDINAL1:def 12;

p . i = |[((f /. j) `1),((f /. (j + 1)) `2)]| by A24, A25, A26, A29, A30;

hence y in the carrier of (TOP-REAL 2) by A27; :: thesis: verum

end;A30: i = (2 * j) + (i mod 2) and

i mod 2 < 2 by NAT_D:def 2;

reconsider j = j as Element of NAT by ORDINAL1:def 12;

p . i = |[((f /. j) `1),((f /. (j + 1)) `2)]| by A24, A25, A26, A29, A30;

hence y in the carrier of (TOP-REAL 2) by A27; :: thesis: verum

suppose A31:
i mod 2 = 1
; :: thesis: y in the carrier of (TOP-REAL 2)

consider j being Nat such that

A32: i = (2 * j) + (i mod 2) and

i mod 2 < 2 by NAT_D:def 2;

reconsider j = j as Element of NAT by ORDINAL1:def 12;

(2 * (j + 1)) -' 1 = (2 * (j + 1)) - 1 by A28, A31, A32, NAT_D:39;

then p . i = f /. (j + 1) by A24, A25, A26, A31, A32;

hence y in the carrier of (TOP-REAL 2) by A27; :: thesis: verum

end;A32: i = (2 * j) + (i mod 2) and

i mod 2 < 2 by NAT_D:def 2;

reconsider j = j as Element of NAT by ORDINAL1:def 12;

(2 * (j + 1)) -' 1 = (2 * (j + 1)) - 1 by A28, A31, A32, NAT_D:39;

then p . i = f /. (j + 1) by A24, A25, A26, A31, A32;

hence y in the carrier of (TOP-REAL 2) by A27; :: thesis: verum

A33: len p = (2 * (len f)) -' 1 by A24, FINSEQ_1:def 3;

for i being Nat st 1 <= i & i + 1 <= len g1 & not (g1 /. i) `1 = (g1 /. (i + 1)) `1 holds

(g1 /. i) `2 = (g1 /. (i + 1)) `2

proof

then A48:
g1 is special
by TOPREAL1:def 5;
let i be Nat; :: thesis: ( 1 <= i & i + 1 <= len g1 & not (g1 /. i) `1 = (g1 /. (i + 1)) `1 implies (g1 /. i) `2 = (g1 /. (i + 1)) `2 )

assume that

A34: 1 <= i and

A35: i + 1 <= len g1 ; :: thesis: ( (g1 /. i) `1 = (g1 /. (i + 1)) `1 or (g1 /. i) `2 = (g1 /. (i + 1)) `2 )

A36: i < len g1 by A35, NAT_1:13;

then A37: g1 . i = g1 /. i by A34, FINSEQ_4:15;

A38: 1 < i + 1 by A34, NAT_1:13;

then A39: i + 1 in Seg (len g1) by A35, FINSEQ_1:1;

A40: i in Seg ((2 * (len f)) -' 1) by A33, A34, A36, FINSEQ_1:1;

A41: g1 . (i + 1) = g1 /. (i + 1) by A35, A38, FINSEQ_4:15;

end;assume that

A34: 1 <= i and

A35: i + 1 <= len g1 ; :: thesis: ( (g1 /. i) `1 = (g1 /. (i + 1)) `1 or (g1 /. i) `2 = (g1 /. (i + 1)) `2 )

A36: i < len g1 by A35, NAT_1:13;

then A37: g1 . i = g1 /. i by A34, FINSEQ_4:15;

A38: 1 < i + 1 by A34, NAT_1:13;

then A39: i + 1 in Seg (len g1) by A35, FINSEQ_1:1;

A40: i in Seg ((2 * (len f)) -' 1) by A33, A34, A36, FINSEQ_1:1;

A41: g1 . (i + 1) = g1 /. (i + 1) by A35, A38, FINSEQ_4:15;

per cases
( i mod 2 = 0 or i mod 2 = 1 )
by NAT_D:12;

end;

suppose A42:
i mod 2 = 0
; :: thesis: ( (g1 /. i) `1 = (g1 /. (i + 1)) `1 or (g1 /. i) `2 = (g1 /. (i + 1)) `2 )

consider j being Nat such that

A43: i = (2 * j) + (i mod 2) and

i mod 2 < 2 by NAT_D:def 2;

reconsider j = j as Element of NAT by ORDINAL1:def 12;

1 <= 1 + i by NAT_1:11;

then (2 * (j + 1)) -' 1 = (2 * (j + 1)) - 1 by A42, A43, NAT_D:39;

then A44: g1 . (i + 1) = f /. (j + 1) by A25, A33, A39, A42, A43;

g1 . i = |[((f /. j) `1),((f /. (j + 1)) `2)]| by A25, A40, A42, A43;

hence ( (g1 /. i) `1 = (g1 /. (i + 1)) `1 or (g1 /. i) `2 = (g1 /. (i + 1)) `2 ) by A37, A41, A44, EUCLID:52; :: thesis: verum

end;A43: i = (2 * j) + (i mod 2) and

i mod 2 < 2 by NAT_D:def 2;

reconsider j = j as Element of NAT by ORDINAL1:def 12;

1 <= 1 + i by NAT_1:11;

then (2 * (j + 1)) -' 1 = (2 * (j + 1)) - 1 by A42, A43, NAT_D:39;

then A44: g1 . (i + 1) = f /. (j + 1) by A25, A33, A39, A42, A43;

g1 . i = |[((f /. j) `1),((f /. (j + 1)) `2)]| by A25, A40, A42, A43;

hence ( (g1 /. i) `1 = (g1 /. (i + 1)) `1 or (g1 /. i) `2 = (g1 /. (i + 1)) `2 ) by A37, A41, A44, EUCLID:52; :: thesis: verum

suppose A45:
i mod 2 = 1
; :: thesis: ( (g1 /. i) `1 = (g1 /. (i + 1)) `1 or (g1 /. i) `2 = (g1 /. (i + 1)) `2 )

consider j being Nat such that

A46: i = (2 * j) + (i mod 2) and

i mod 2 < 2 by NAT_D:def 2;

reconsider j = j as Element of NAT by ORDINAL1:def 12;

i + 1 = 2 * (j + 1) by A45, A46;

then A47: g1 . (i + 1) = |[((f /. (j + 1)) `1),((f /. ((j + 1) + 1)) `2)]| by A25, A33, A39;

(2 * (j + 1)) -' 1 = (2 * (j + 1)) - 1 by A34, A45, A46, NAT_D:39;

then g1 . i = f /. (j + 1) by A25, A40, A45, A46;

hence ( (g1 /. i) `1 = (g1 /. (i + 1)) `1 or (g1 /. i) `2 = (g1 /. (i + 1)) `2 ) by A37, A41, A47, EUCLID:52; :: thesis: verum

end;A46: i = (2 * j) + (i mod 2) and

i mod 2 < 2 by NAT_D:def 2;

reconsider j = j as Element of NAT by ORDINAL1:def 12;

i + 1 = 2 * (j + 1) by A45, A46;

then A47: g1 . (i + 1) = |[((f /. (j + 1)) `1),((f /. ((j + 1) + 1)) `2)]| by A25, A33, A39;

(2 * (j + 1)) -' 1 = (2 * (j + 1)) - 1 by A34, A45, A46, NAT_D:39;

then g1 . i = f /. (j + 1) by A25, A40, A45, A46;

hence ( (g1 /. i) `1 = (g1 /. (i + 1)) `1 or (g1 /. i) `2 = (g1 /. (i + 1)) `2 ) by A37, A41, A47, EUCLID:52; :: thesis: verum

A49: 2 * (len f) >= 2 * 1 by A1, XREAL_1:64;

then A50: (2 * (len f)) -' 1 = (2 * (len f)) - 1 by XREAL_1:233, XXREAL_0:2;

for i being Nat st i in dom (Y_axis g1) holds

( c <= (Y_axis g1) . i & (Y_axis g1) . i <= d )

proof

then A67:
Y_axis g1 lies_between c,d
by GOBOARD4:def 2;
let i be Nat; :: thesis: ( i in dom (Y_axis g1) implies ( c <= (Y_axis g1) . i & (Y_axis g1) . i <= d ) )

A51: len (Y_axis f) = len f by GOBOARD1:def 2;

assume A52: i in dom (Y_axis g1) ; :: thesis: ( c <= (Y_axis g1) . i & (Y_axis g1) . i <= d )

then A53: i in Seg (len (Y_axis g1)) by FINSEQ_1:def 3;

then A54: i in Seg (len g1) by GOBOARD1:def 2;

i in Seg (len g1) by A53, GOBOARD1:def 2;

then A55: i <= len g1 by FINSEQ_1:1;

A56: 1 <= i by A53, FINSEQ_1:1;

then A57: g1 /. i = g1 . i by A55, FINSEQ_4:15;

A58: (Y_axis g1) . i = (g1 /. i) `2 by A52, GOBOARD1:def 2;

end;A51: len (Y_axis f) = len f by GOBOARD1:def 2;

assume A52: i in dom (Y_axis g1) ; :: thesis: ( c <= (Y_axis g1) . i & (Y_axis g1) . i <= d )

then A53: i in Seg (len (Y_axis g1)) by FINSEQ_1:def 3;

then A54: i in Seg (len g1) by GOBOARD1:def 2;

i in Seg (len g1) by A53, GOBOARD1:def 2;

then A55: i <= len g1 by FINSEQ_1:1;

A56: 1 <= i by A53, FINSEQ_1:1;

then A57: g1 /. i = g1 . i by A55, FINSEQ_4:15;

A58: (Y_axis g1) . i = (g1 /. i) `2 by A52, GOBOARD1:def 2;

per cases
( i mod 2 = 0 or i mod 2 = 1 )
by NAT_D:12;

end;

suppose A59:
i mod 2 = 0
; :: thesis: ( c <= (Y_axis g1) . i & (Y_axis g1) . i <= d )

consider j being Nat such that

A60: i = (2 * j) + (i mod 2) and

i mod 2 < 2 by NAT_D:def 2;

reconsider j = j as Element of NAT by ORDINAL1:def 12;

g1 . i = |[((f /. j) `1),((f /. (j + 1)) `2)]| by A25, A33, A54, A59, A60;

then A61: (g1 /. i) `2 = (f /. (j + 1)) `2 by A57, EUCLID:52;

(2 * j) + 1 <= ((2 * (len f)) - 1) + 1 by A33, A50, A55, A59, A60, XREAL_1:6;

then 2 * j < 2 * (len f) by NAT_1:13;

then (2 * j) / 2 < (2 * (len f)) / 2 by XREAL_1:74;

then ( 1 <= j + 1 & j + 1 <= len f ) by NAT_1:11, NAT_1:13;

then j + 1 in Seg (len f) by FINSEQ_1:1;

then A62: j + 1 in dom (Y_axis f) by A51, FINSEQ_1:def 3;

then (Y_axis f) . (j + 1) = (f /. (j + 1)) `2 by GOBOARD1:def 2;

hence ( c <= (Y_axis g1) . i & (Y_axis g1) . i <= d ) by A3, A58, A61, A62, GOBOARD4:def 2; :: thesis: verum

end;A60: i = (2 * j) + (i mod 2) and

i mod 2 < 2 by NAT_D:def 2;

reconsider j = j as Element of NAT by ORDINAL1:def 12;

g1 . i = |[((f /. j) `1),((f /. (j + 1)) `2)]| by A25, A33, A54, A59, A60;

then A61: (g1 /. i) `2 = (f /. (j + 1)) `2 by A57, EUCLID:52;

(2 * j) + 1 <= ((2 * (len f)) - 1) + 1 by A33, A50, A55, A59, A60, XREAL_1:6;

then 2 * j < 2 * (len f) by NAT_1:13;

then (2 * j) / 2 < (2 * (len f)) / 2 by XREAL_1:74;

then ( 1 <= j + 1 & j + 1 <= len f ) by NAT_1:11, NAT_1:13;

then j + 1 in Seg (len f) by FINSEQ_1:1;

then A62: j + 1 in dom (Y_axis f) by A51, FINSEQ_1:def 3;

then (Y_axis f) . (j + 1) = (f /. (j + 1)) `2 by GOBOARD1:def 2;

hence ( c <= (Y_axis g1) . i & (Y_axis g1) . i <= d ) by A3, A58, A61, A62, GOBOARD4:def 2; :: thesis: verum

suppose A63:
i mod 2 = 1
; :: thesis: ( c <= (Y_axis g1) . i & (Y_axis g1) . i <= d )

consider j being Nat such that

A64: i = (2 * j) + (i mod 2) and

i mod 2 < 2 by NAT_D:def 2;

reconsider j = j as Element of NAT by ORDINAL1:def 12;

(2 * (j + 1)) -' 1 = (2 * (j + 1)) - 1 by A56, A63, A64, NAT_D:39;

then A65: (g1 /. i) `2 = (f /. (j + 1)) `2 by A25, A33, A54, A57, A63, A64;

(2 * j) + 1 <= ((2 * (len f)) - 1) + 1 by A33, A50, A55, A63, A64, NAT_1:13;

then 2 * j < 2 * (len f) by NAT_1:13;

then (2 * j) / 2 < (2 * (len f)) / 2 by XREAL_1:74;

then ( 1 <= j + 1 & j + 1 <= len f ) by NAT_1:11, NAT_1:13;

then j + 1 in Seg (len f) by FINSEQ_1:1;

then A66: j + 1 in dom (Y_axis f) by A51, FINSEQ_1:def 3;

then (Y_axis f) . (j + 1) = (f /. (j + 1)) `2 by GOBOARD1:def 2;

hence ( c <= (Y_axis g1) . i & (Y_axis g1) . i <= d ) by A3, A58, A65, A66, GOBOARD4:def 2; :: thesis: verum

end;A64: i = (2 * j) + (i mod 2) and

i mod 2 < 2 by NAT_D:def 2;

reconsider j = j as Element of NAT by ORDINAL1:def 12;

(2 * (j + 1)) -' 1 = (2 * (j + 1)) - 1 by A56, A63, A64, NAT_D:39;

then A65: (g1 /. i) `2 = (f /. (j + 1)) `2 by A25, A33, A54, A57, A63, A64;

(2 * j) + 1 <= ((2 * (len f)) - 1) + 1 by A33, A50, A55, A63, A64, NAT_1:13;

then 2 * j < 2 * (len f) by NAT_1:13;

then (2 * j) / 2 < (2 * (len f)) / 2 by XREAL_1:74;

then ( 1 <= j + 1 & j + 1 <= len f ) by NAT_1:11, NAT_1:13;

then j + 1 in Seg (len f) by FINSEQ_1:1;

then A66: j + 1 in dom (Y_axis f) by A51, FINSEQ_1:def 3;

then (Y_axis f) . (j + 1) = (f /. (j + 1)) `2 by GOBOARD1:def 2;

hence ( c <= (Y_axis g1) . i & (Y_axis g1) . i <= d ) by A3, A58, A65, A66, GOBOARD4:def 2; :: thesis: verum

for i being Nat st i in dom (X_axis g1) holds

( (X_axis f) . 1 <= (X_axis g1) . i & (X_axis g1) . i <= (X_axis f) . (len f) )

proof

then A85:
X_axis g1 lies_between (X_axis f) . 1,(X_axis f) . (len f)
by GOBOARD4:def 2;
let i be Nat; :: thesis: ( i in dom (X_axis g1) implies ( (X_axis f) . 1 <= (X_axis g1) . i & (X_axis g1) . i <= (X_axis f) . (len f) ) )

A68: len (X_axis f) = len f by GOBOARD1:def 1;

assume A69: i in dom (X_axis g1) ; :: thesis: ( (X_axis f) . 1 <= (X_axis g1) . i & (X_axis g1) . i <= (X_axis f) . (len f) )

then A70: i in Seg (len (X_axis g1)) by FINSEQ_1:def 3;

then A71: i in Seg (len g1) by GOBOARD1:def 1;

i in Seg (len g1) by A70, GOBOARD1:def 1;

then A72: i <= len g1 by FINSEQ_1:1;

A73: 1 <= i by A70, FINSEQ_1:1;

then A74: g1 /. i = g1 . i by A72, FINSEQ_4:15;

A75: (X_axis g1) . i = (g1 /. i) `1 by A69, GOBOARD1:def 1;

end;A68: len (X_axis f) = len f by GOBOARD1:def 1;

assume A69: i in dom (X_axis g1) ; :: thesis: ( (X_axis f) . 1 <= (X_axis g1) . i & (X_axis g1) . i <= (X_axis f) . (len f) )

then A70: i in Seg (len (X_axis g1)) by FINSEQ_1:def 3;

then A71: i in Seg (len g1) by GOBOARD1:def 1;

i in Seg (len g1) by A70, GOBOARD1:def 1;

then A72: i <= len g1 by FINSEQ_1:1;

A73: 1 <= i by A70, FINSEQ_1:1;

then A74: g1 /. i = g1 . i by A72, FINSEQ_4:15;

A75: (X_axis g1) . i = (g1 /. i) `1 by A69, GOBOARD1:def 1;

per cases
( i mod 2 = 0 or i mod 2 = 1 )
by NAT_D:12;

end;

suppose A76:
i mod 2 = 0
; :: thesis: ( (X_axis f) . 1 <= (X_axis g1) . i & (X_axis g1) . i <= (X_axis f) . (len f) )

consider j being Nat such that

A77: i = (2 * j) + (i mod 2) and

i mod 2 < 2 by NAT_D:def 2;

reconsider j = j as Element of NAT by ORDINAL1:def 12;

g1 . i = |[((f /. j) `1),((f /. (j + 1)) `2)]| by A25, A33, A71, A76, A77;

then A78: (g1 /. i) `1 = (f /. j) `1 by A74, EUCLID:52;

(2 * j) + 1 <= ((2 * (len f)) - 1) + 1 by A33, A50, A72, A76, A77, XREAL_1:6;

then 2 * j < 2 * (len f) by NAT_1:13;

then A79: (2 * j) / 2 < (2 * (len f)) / 2 by XREAL_1:74;

j > 0 by A70, A76, A77, FINSEQ_1:1;

then j >= 0 + 1 by NAT_1:13;

then j in Seg (len f) by A79, FINSEQ_1:1;

then A80: j in dom (X_axis f) by A68, FINSEQ_1:def 3;

then (X_axis f) . j = (f /. j) `1 by GOBOARD1:def 1;

hence ( (X_axis f) . 1 <= (X_axis g1) . i & (X_axis g1) . i <= (X_axis f) . (len f) ) by A2, A75, A78, A80, GOBOARD4:def 2; :: thesis: verum

end;A77: i = (2 * j) + (i mod 2) and

i mod 2 < 2 by NAT_D:def 2;

reconsider j = j as Element of NAT by ORDINAL1:def 12;

g1 . i = |[((f /. j) `1),((f /. (j + 1)) `2)]| by A25, A33, A71, A76, A77;

then A78: (g1 /. i) `1 = (f /. j) `1 by A74, EUCLID:52;

(2 * j) + 1 <= ((2 * (len f)) - 1) + 1 by A33, A50, A72, A76, A77, XREAL_1:6;

then 2 * j < 2 * (len f) by NAT_1:13;

then A79: (2 * j) / 2 < (2 * (len f)) / 2 by XREAL_1:74;

j > 0 by A70, A76, A77, FINSEQ_1:1;

then j >= 0 + 1 by NAT_1:13;

then j in Seg (len f) by A79, FINSEQ_1:1;

then A80: j in dom (X_axis f) by A68, FINSEQ_1:def 3;

then (X_axis f) . j = (f /. j) `1 by GOBOARD1:def 1;

hence ( (X_axis f) . 1 <= (X_axis g1) . i & (X_axis g1) . i <= (X_axis f) . (len f) ) by A2, A75, A78, A80, GOBOARD4:def 2; :: thesis: verum

suppose A81:
i mod 2 = 1
; :: thesis: ( (X_axis f) . 1 <= (X_axis g1) . i & (X_axis g1) . i <= (X_axis f) . (len f) )

consider j being Nat such that

A82: i = (2 * j) + (i mod 2) and

i mod 2 < 2 by NAT_D:def 2;

reconsider j = j as Element of NAT by ORDINAL1:def 12;

(2 * (j + 1)) -' 1 = (2 * (j + 1)) - 1 by A73, A81, A82, NAT_D:39;

then A83: (g1 /. i) `1 = (f /. (j + 1)) `1 by A25, A33, A71, A74, A81, A82;

(2 * j) + 1 <= ((2 * (len f)) - 1) + 1 by A33, A50, A72, A81, A82, NAT_1:13;

then 2 * j < 2 * (len f) by NAT_1:13;

then (2 * j) / 2 < (2 * (len f)) / 2 by XREAL_1:74;

then ( 1 <= j + 1 & j + 1 <= len f ) by NAT_1:11, NAT_1:13;

then j + 1 in Seg (len f) by FINSEQ_1:1;

then A84: j + 1 in dom (X_axis f) by A68, FINSEQ_1:def 3;

then (X_axis f) . (j + 1) = (f /. (j + 1)) `1 by GOBOARD1:def 1;

hence ( (X_axis f) . 1 <= (X_axis g1) . i & (X_axis g1) . i <= (X_axis f) . (len f) ) by A2, A75, A83, A84, GOBOARD4:def 2; :: thesis: verum

end;A82: i = (2 * j) + (i mod 2) and

i mod 2 < 2 by NAT_D:def 2;

reconsider j = j as Element of NAT by ORDINAL1:def 12;

(2 * (j + 1)) -' 1 = (2 * (j + 1)) - 1 by A73, A81, A82, NAT_D:39;

then A83: (g1 /. i) `1 = (f /. (j + 1)) `1 by A25, A33, A71, A74, A81, A82;

(2 * j) + 1 <= ((2 * (len f)) - 1) + 1 by A33, A50, A72, A81, A82, NAT_1:13;

then 2 * j < 2 * (len f) by NAT_1:13;

then (2 * j) / 2 < (2 * (len f)) / 2 by XREAL_1:74;

then ( 1 <= j + 1 & j + 1 <= len f ) by NAT_1:11, NAT_1:13;

then j + 1 in Seg (len f) by FINSEQ_1:1;

then A84: j + 1 in dom (X_axis f) by A68, FINSEQ_1:def 3;

then (X_axis f) . (j + 1) = (f /. (j + 1)) `1 by GOBOARD1:def 1;

hence ( (X_axis f) . 1 <= (X_axis g1) . i & (X_axis g1) . i <= (X_axis f) . (len f) ) by A2, A75, A83, A84, GOBOARD4:def 2; :: thesis: verum

(len f) + (len f) >= (len f) + 1 by A1, XREAL_1:6;

then A86: (2 * (len f)) - 1 >= ((len f) + 1) - 1 by XREAL_1:9;

A87: (2 * 1) -' 1 = (1 + 1) -' 1

.= 1 by NAT_D:34 ;

A88: (2 * (len f)) - 1 >= (1 + 1) - 1 by A49, XREAL_1:9;

then 1 in Seg ((2 * (len f)) -' 1) by A50, FINSEQ_1:1;

then A89: p . 1 = f /. 1 by A25, A87;

A90: for i being Nat st 1 <= i & i + 1 <= len g1 holds

|.((g1 /. i) - (g1 /. (i + 1))).| < a

proof

A114:
for i being Nat st i in dom g1 holds
let i be Nat; :: thesis: ( 1 <= i & i + 1 <= len g1 implies |.((g1 /. i) - (g1 /. (i + 1))).| < a )

assume that

A91: 1 <= i and

A92: i + 1 <= len g1 ; :: thesis: |.((g1 /. i) - (g1 /. (i + 1))).| < a

A93: g1 . (i + 1) = g1 /. (i + 1) by A92, FINSEQ_4:15, NAT_1:11;

i <= len g1 by A92, NAT_1:13;

then A94: i in Seg (len g1) by A91, FINSEQ_1:1;

i <= len g1 by A92, NAT_1:13;

then A95: g1 . i = g1 /. i by A91, FINSEQ_4:15;

1 <= i + 1 by NAT_1:11;

then A96: i + 1 in Seg ((2 * (len f)) -' 1) by A33, A92, FINSEQ_1:1;

end;assume that

A91: 1 <= i and

A92: i + 1 <= len g1 ; :: thesis: |.((g1 /. i) - (g1 /. (i + 1))).| < a

A93: g1 . (i + 1) = g1 /. (i + 1) by A92, FINSEQ_4:15, NAT_1:11;

i <= len g1 by A92, NAT_1:13;

then A94: i in Seg (len g1) by A91, FINSEQ_1:1;

i <= len g1 by A92, NAT_1:13;

then A95: g1 . i = g1 /. i by A91, FINSEQ_4:15;

1 <= i + 1 by NAT_1:11;

then A96: i + 1 in Seg ((2 * (len f)) -' 1) by A33, A92, FINSEQ_1:1;

per cases
( i mod 2 = 0 or i mod 2 = 1 )
by NAT_D:12;

end;

suppose A97:
i mod 2 = 0
; :: thesis: |.((g1 /. i) - (g1 /. (i + 1))).| < a

consider j being Nat such that

A98: i = (2 * j) + (i mod 2) and

i mod 2 < 2 by NAT_D:def 2;

reconsider j = j as Element of NAT by ORDINAL1:def 12;

A99: g1 . i = |[((f /. j) `1),((f /. (j + 1)) `2)]| by A25, A33, A94, A97, A98;

then A100: (g1 /. i) `2 = (f /. (j + 1)) `2 by A95, EUCLID:52;

1 <= 1 + i by NAT_1:11;

then (2 * (j + 1)) -' 1 = (2 * (j + 1)) - 1 by A97, A98, NAT_D:39;

then g1 . (i + 1) = f /. (j + 1) by A25, A96, A97, A98;

then A101: ( (g1 /. (i + 1)) `1 = (f /. (j + 1)) `1 & (g1 /. (i + 1)) `2 = (f /. (j + 1)) `2 ) by A92, FINSEQ_4:15, NAT_1:11;

A102: (g1 /. i) - (g1 /. (i + 1)) = |[(((g1 /. i) `1) - ((g1 /. (i + 1)) `1)),(((g1 /. i) `2) - ((g1 /. (i + 1)) `2))]| by EUCLID:61

.= |[(((f /. j) `1) - ((f /. (j + 1)) `1)),0]| by A95, A99, A100, A101, EUCLID:52 ;

then A103: ((g1 /. i) - (g1 /. (i + 1))) `1 = ((f /. j) `1) - ((f /. (j + 1)) `1) by EUCLID:52;

(2 * j) + 1 <= ((2 * (len f)) - 1) + 1 by A33, A50, A92, A97, A98, NAT_1:13;

then 2 * j < 2 * (len f) by NAT_1:13;

then (2 * j) / 2 < (2 * (len f)) / 2 by XREAL_1:74;

then A104: j + 1 <= len f by NAT_1:13;

|.((g1 /. i) - (g1 /. (i + 1))).| = sqrt (((((g1 /. i) - (g1 /. (i + 1))) `1) ^2) + ((((g1 /. i) - (g1 /. (i + 1))) `2) ^2)) by Th30

.= sqrt (((((f /. j) `1) - ((f /. (j + 1)) `1)) ^2) + (0 ^2)) by A102, A103, EUCLID:52

.= sqrt ((((f /. j) `1) - ((f /. (j + 1)) `1)) ^2) ;

then |.((g1 /. i) - (g1 /. (i + 1))).| = |.(((f /. j) `1) - ((f /. (j + 1)) `1)).| by COMPLEX1:72;

then A105: |.((g1 /. i) - (g1 /. (i + 1))).| <= |.((f /. j) - (f /. (j + 1))).| by Th34;

j > 0 by A91, A97, A98;

then j >= 0 + 1 by NAT_1:13;

then |.((f /. j) - (f /. (j + 1))).| < a by A5, A104;

hence |.((g1 /. i) - (g1 /. (i + 1))).| < a by A105, XXREAL_0:2; :: thesis: verum

end;A98: i = (2 * j) + (i mod 2) and

i mod 2 < 2 by NAT_D:def 2;

reconsider j = j as Element of NAT by ORDINAL1:def 12;

A99: g1 . i = |[((f /. j) `1),((f /. (j + 1)) `2)]| by A25, A33, A94, A97, A98;

then A100: (g1 /. i) `2 = (f /. (j + 1)) `2 by A95, EUCLID:52;

1 <= 1 + i by NAT_1:11;

then (2 * (j + 1)) -' 1 = (2 * (j + 1)) - 1 by A97, A98, NAT_D:39;

then g1 . (i + 1) = f /. (j + 1) by A25, A96, A97, A98;

then A101: ( (g1 /. (i + 1)) `1 = (f /. (j + 1)) `1 & (g1 /. (i + 1)) `2 = (f /. (j + 1)) `2 ) by A92, FINSEQ_4:15, NAT_1:11;

A102: (g1 /. i) - (g1 /. (i + 1)) = |[(((g1 /. i) `1) - ((g1 /. (i + 1)) `1)),(((g1 /. i) `2) - ((g1 /. (i + 1)) `2))]| by EUCLID:61

.= |[(((f /. j) `1) - ((f /. (j + 1)) `1)),0]| by A95, A99, A100, A101, EUCLID:52 ;

then A103: ((g1 /. i) - (g1 /. (i + 1))) `1 = ((f /. j) `1) - ((f /. (j + 1)) `1) by EUCLID:52;

(2 * j) + 1 <= ((2 * (len f)) - 1) + 1 by A33, A50, A92, A97, A98, NAT_1:13;

then 2 * j < 2 * (len f) by NAT_1:13;

then (2 * j) / 2 < (2 * (len f)) / 2 by XREAL_1:74;

then A104: j + 1 <= len f by NAT_1:13;

|.((g1 /. i) - (g1 /. (i + 1))).| = sqrt (((((g1 /. i) - (g1 /. (i + 1))) `1) ^2) + ((((g1 /. i) - (g1 /. (i + 1))) `2) ^2)) by Th30

.= sqrt (((((f /. j) `1) - ((f /. (j + 1)) `1)) ^2) + (0 ^2)) by A102, A103, EUCLID:52

.= sqrt ((((f /. j) `1) - ((f /. (j + 1)) `1)) ^2) ;

then |.((g1 /. i) - (g1 /. (i + 1))).| = |.(((f /. j) `1) - ((f /. (j + 1)) `1)).| by COMPLEX1:72;

then A105: |.((g1 /. i) - (g1 /. (i + 1))).| <= |.((f /. j) - (f /. (j + 1))).| by Th34;

j > 0 by A91, A97, A98;

then j >= 0 + 1 by NAT_1:13;

then |.((f /. j) - (f /. (j + 1))).| < a by A5, A104;

hence |.((g1 /. i) - (g1 /. (i + 1))).| < a by A105, XXREAL_0:2; :: thesis: verum

suppose A106:
i mod 2 = 1
; :: thesis: |.((g1 /. i) - (g1 /. (i + 1))).| < a

consider j being Nat such that

A107: i = (2 * j) + (i mod 2) and

i mod 2 < 2 by NAT_D:def 2;

reconsider j = j as Element of NAT by ORDINAL1:def 12;

(2 * (j + 1)) -' 1 = (2 * (j + 1)) - 1 by A91, A106, A107, NAT_D:39;

then A108: ( (g1 /. i) `1 = (f /. (j + 1)) `1 & (g1 /. i) `2 = (f /. (j + 1)) `2 ) by A25, A33, A94, A95, A106, A107;

i + 1 = 2 * (j + 1) by A106, A107;

then A109: g1 /. (i + 1) = |[((f /. (j + 1)) `1),((f /. ((j + 1) + 1)) `2)]| by A25, A96, A93;

then A110: (g1 /. (i + 1)) `1 = (f /. (j + 1)) `1 by EUCLID:52;

A111: (g1 /. i) - (g1 /. (i + 1)) = |[(((g1 /. i) `1) - ((g1 /. (i + 1)) `1)),(((g1 /. i) `2) - ((g1 /. (i + 1)) `2))]| by EUCLID:61

.= |[0,(((f /. (j + 1)) `2) - ((f /. ((j + 1) + 1)) `2))]| by A109, A110, A108, EUCLID:52 ;

then A112: ((g1 /. i) - (g1 /. (i + 1))) `1 = 0 by EUCLID:52;

(2 * (j + 1)) + 1 <= ((2 * (len f)) - 1) + 1 by A33, A50, A92, A106, A107, XREAL_1:6;

then 2 * (j + 1) < 2 * (len f) by NAT_1:13;

then (2 * (j + 1)) / 2 < (2 * (len f)) / 2 by XREAL_1:74;

then (j + 1) + 1 <= len f by NAT_1:13;

then A113: |.((f /. (j + 1)) - (f /. ((j + 1) + 1))).| < a by A5, NAT_1:11;

|.((g1 /. i) - (g1 /. (i + 1))).| = sqrt (((((g1 /. i) - (g1 /. (i + 1))) `1) ^2) + ((((g1 /. i) - (g1 /. (i + 1))) `2) ^2)) by Th30

.= sqrt ((((f /. (j + 1)) `2) - ((f /. ((j + 1) + 1)) `2)) ^2) by A111, A112, EUCLID:52 ;

then |.((g1 /. i) - (g1 /. (i + 1))).| = |.(((f /. (j + 1)) `2) - ((f /. ((j + 1) + 1)) `2)).| by COMPLEX1:72;

then |.((g1 /. i) - (g1 /. (i + 1))).| <= |.((f /. (j + 1)) - (f /. ((j + 1) + 1))).| by Th34;

hence |.((g1 /. i) - (g1 /. (i + 1))).| < a by A113, XXREAL_0:2; :: thesis: verum

end;A107: i = (2 * j) + (i mod 2) and

i mod 2 < 2 by NAT_D:def 2;

reconsider j = j as Element of NAT by ORDINAL1:def 12;

(2 * (j + 1)) -' 1 = (2 * (j + 1)) - 1 by A91, A106, A107, NAT_D:39;

then A108: ( (g1 /. i) `1 = (f /. (j + 1)) `1 & (g1 /. i) `2 = (f /. (j + 1)) `2 ) by A25, A33, A94, A95, A106, A107;

i + 1 = 2 * (j + 1) by A106, A107;

then A109: g1 /. (i + 1) = |[((f /. (j + 1)) `1),((f /. ((j + 1) + 1)) `2)]| by A25, A96, A93;

then A110: (g1 /. (i + 1)) `1 = (f /. (j + 1)) `1 by EUCLID:52;

A111: (g1 /. i) - (g1 /. (i + 1)) = |[(((g1 /. i) `1) - ((g1 /. (i + 1)) `1)),(((g1 /. i) `2) - ((g1 /. (i + 1)) `2))]| by EUCLID:61

.= |[0,(((f /. (j + 1)) `2) - ((f /. ((j + 1) + 1)) `2))]| by A109, A110, A108, EUCLID:52 ;

then A112: ((g1 /. i) - (g1 /. (i + 1))) `1 = 0 by EUCLID:52;

(2 * (j + 1)) + 1 <= ((2 * (len f)) - 1) + 1 by A33, A50, A92, A106, A107, XREAL_1:6;

then 2 * (j + 1) < 2 * (len f) by NAT_1:13;

then (2 * (j + 1)) / 2 < (2 * (len f)) / 2 by XREAL_1:74;

then (j + 1) + 1 <= len f by NAT_1:13;

then A113: |.((f /. (j + 1)) - (f /. ((j + 1) + 1))).| < a by A5, NAT_1:11;

|.((g1 /. i) - (g1 /. (i + 1))).| = sqrt (((((g1 /. i) - (g1 /. (i + 1))) `1) ^2) + ((((g1 /. i) - (g1 /. (i + 1))) `2) ^2)) by Th30

.= sqrt ((((f /. (j + 1)) `2) - ((f /. ((j + 1) + 1)) `2)) ^2) by A111, A112, EUCLID:52 ;

then |.((g1 /. i) - (g1 /. (i + 1))).| = |.(((f /. (j + 1)) `2) - ((f /. ((j + 1) + 1)) `2)).| by COMPLEX1:72;

then |.((g1 /. i) - (g1 /. (i + 1))).| <= |.((f /. (j + 1)) - (f /. ((j + 1) + 1))).| by Th34;

hence |.((g1 /. i) - (g1 /. (i + 1))).| < a by A113, XXREAL_0:2; :: thesis: verum

ex k being Nat st

( k in dom f & |.((g1 /. i) - (f /. k)).| < a )

proof

(2 * (len f)) -' 1 in Seg ((2 * (len f)) -' 1)
by A50, A88, FINSEQ_1:1;
let i be Nat; :: thesis: ( i in dom g1 implies ex k being Nat st

( k in dom f & |.((g1 /. i) - (f /. k)).| < a ) )

assume A115: i in dom g1 ; :: thesis: ex k being Nat st

( k in dom f & |.((g1 /. i) - (f /. k)).| < a )

then A116: i in Seg (len g1) by FINSEQ_1:def 3;

then A117: i <= len g1 by FINSEQ_1:1;

A118: 1 <= i by A116, FINSEQ_1:1;

then A119: g1 . i = g1 /. i by A117, FINSEQ_4:15;

end;( k in dom f & |.((g1 /. i) - (f /. k)).| < a ) )

assume A115: i in dom g1 ; :: thesis: ex k being Nat st

( k in dom f & |.((g1 /. i) - (f /. k)).| < a )

then A116: i in Seg (len g1) by FINSEQ_1:def 3;

then A117: i <= len g1 by FINSEQ_1:1;

A118: 1 <= i by A116, FINSEQ_1:1;

then A119: g1 . i = g1 /. i by A117, FINSEQ_4:15;

per cases
( i mod 2 = 0 or i mod 2 = 1 )
by NAT_D:12;

end;

suppose A120:
i mod 2 = 0
; :: thesis: ex k being Nat st

( k in dom f & |.((g1 /. i) - (f /. k)).| < a )

( k in dom f & |.((g1 /. i) - (f /. k)).| < a )

consider j being Nat such that

A121: i = (2 * j) + (i mod 2) and

i mod 2 < 2 by NAT_D:def 2;

reconsider j = j as Element of NAT by ORDINAL1:def 12;

j > 0 by A116, A120, A121, FINSEQ_1:1;

then A122: j >= 0 + 1 by NAT_1:13;

A123: g1 . i = |[((f /. j) `1),((f /. (j + 1)) `2)]| by A24, A25, A115, A120, A121;

then A124: (g1 /. i) `1 = (f /. j) `1 by A119, EUCLID:52;

A125: (g1 /. i) `2 = (f /. (j + 1)) `2 by A119, A123, EUCLID:52;

A126: (g1 /. i) - (f /. j) = |[(((g1 /. i) `1) - ((f /. j) `1)),(((g1 /. i) `2) - ((f /. j) `2))]| by EUCLID:61

.= |[0,(((g1 /. i) `2) - ((f /. j) `2))]| by A124 ;

then ((g1 /. i) - (f /. j)) `2 = ((g1 /. i) `2) - ((f /. j) `2) by EUCLID:52;

then |.((g1 /. i) - (f /. j)).| = sqrt (((((g1 /. i) - (f /. j)) `1) ^2) + ((((g1 /. i) `2) - ((f /. j) `2)) ^2)) by Th30

.= sqrt ((0 ^2) + ((((f /. (j + 1)) `2) - ((f /. j) `2)) ^2)) by A125, A126, EUCLID:52

.= sqrt ((((f /. (j + 1)) `2) - ((f /. j) `2)) ^2) ;

then |.((g1 /. i) - (f /. j)).| = |.(((f /. (j + 1)) `2) - ((f /. j) `2)).| by COMPLEX1:72

.= |.(((f /. j) `2) - ((f /. (j + 1)) `2)).| by UNIFORM1:11 ;

then A127: |.((g1 /. i) - (f /. j)).| <= |.((f /. j) - (f /. (j + 1))).| by Th34;

(2 * j) + 1 <= ((2 * (len f)) - 1) + 1 by A33, A50, A117, A120, A121, XREAL_1:6;

then 2 * j < 2 * (len f) by NAT_1:13;

then A128: (2 * j) / 2 < (2 * (len f)) / 2 by XREAL_1:74;

then j + 1 <= len f by NAT_1:13;

then |.((f /. j) - (f /. (j + 1))).| < a by A5, A122;

then A129: |.((g1 /. i) - (f /. j)).| < a by A127, XXREAL_0:2;

j in dom f by A122, A128, FINSEQ_3:25;

hence ex k being Nat st

( k in dom f & |.((g1 /. i) - (f /. k)).| < a ) by A129; :: thesis: verum

end;A121: i = (2 * j) + (i mod 2) and

i mod 2 < 2 by NAT_D:def 2;

reconsider j = j as Element of NAT by ORDINAL1:def 12;

j > 0 by A116, A120, A121, FINSEQ_1:1;

then A122: j >= 0 + 1 by NAT_1:13;

A123: g1 . i = |[((f /. j) `1),((f /. (j + 1)) `2)]| by A24, A25, A115, A120, A121;

then A124: (g1 /. i) `1 = (f /. j) `1 by A119, EUCLID:52;

A125: (g1 /. i) `2 = (f /. (j + 1)) `2 by A119, A123, EUCLID:52;

A126: (g1 /. i) - (f /. j) = |[(((g1 /. i) `1) - ((f /. j) `1)),(((g1 /. i) `2) - ((f /. j) `2))]| by EUCLID:61

.= |[0,(((g1 /. i) `2) - ((f /. j) `2))]| by A124 ;

then ((g1 /. i) - (f /. j)) `2 = ((g1 /. i) `2) - ((f /. j) `2) by EUCLID:52;

then |.((g1 /. i) - (f /. j)).| = sqrt (((((g1 /. i) - (f /. j)) `1) ^2) + ((((g1 /. i) `2) - ((f /. j) `2)) ^2)) by Th30

.= sqrt ((0 ^2) + ((((f /. (j + 1)) `2) - ((f /. j) `2)) ^2)) by A125, A126, EUCLID:52

.= sqrt ((((f /. (j + 1)) `2) - ((f /. j) `2)) ^2) ;

then |.((g1 /. i) - (f /. j)).| = |.(((f /. (j + 1)) `2) - ((f /. j) `2)).| by COMPLEX1:72

.= |.(((f /. j) `2) - ((f /. (j + 1)) `2)).| by UNIFORM1:11 ;

then A127: |.((g1 /. i) - (f /. j)).| <= |.((f /. j) - (f /. (j + 1))).| by Th34;

(2 * j) + 1 <= ((2 * (len f)) - 1) + 1 by A33, A50, A117, A120, A121, XREAL_1:6;

then 2 * j < 2 * (len f) by NAT_1:13;

then A128: (2 * j) / 2 < (2 * (len f)) / 2 by XREAL_1:74;

then j + 1 <= len f by NAT_1:13;

then |.((f /. j) - (f /. (j + 1))).| < a by A5, A122;

then A129: |.((g1 /. i) - (f /. j)).| < a by A127, XXREAL_0:2;

j in dom f by A122, A128, FINSEQ_3:25;

hence ex k being Nat st

( k in dom f & |.((g1 /. i) - (f /. k)).| < a ) by A129; :: thesis: verum

suppose A130:
i mod 2 = 1
; :: thesis: ex k being Nat st

( k in dom f & |.((g1 /. i) - (f /. k)).| < a )

( k in dom f & |.((g1 /. i) - (f /. k)).| < a )

consider j being Nat such that

A131: i = (2 * j) + (i mod 2) and

i mod 2 < 2 by NAT_D:def 2;

reconsider j = j as Element of NAT by ORDINAL1:def 12;

(2 * (j + 1)) -' 1 = (2 * (j + 1)) - 1 by A118, A130, A131, NAT_D:39;

then g1 . i = f /. (j + 1) by A24, A25, A115, A130, A131;

then A132: |.((g1 /. i) - (f /. (j + 1))).| = |.(0. (TOP-REAL 2)).| by A119, RLVECT_1:5

.= 0 by TOPRNS_1:23 ;

((2 * j) + 1) + 1 <= ((2 * (len f)) - 1) + 1 by A33, A50, A117, A130, A131, XREAL_1:6;

then (2 * j) + 1 < 2 * (len f) by NAT_1:13;

then 2 * j < 2 * (len f) by NAT_1:13;

then (2 * j) / 2 < (2 * (len f)) / 2 by XREAL_1:74;

then A133: j + 1 <= len f by NAT_1:13;

1 <= j + 1 by NAT_1:11;

then j + 1 in dom f by A133, FINSEQ_3:25;

hence ex k being Nat st

( k in dom f & |.((g1 /. i) - (f /. k)).| < a ) by A4, A132; :: thesis: verum

end;A131: i = (2 * j) + (i mod 2) and

i mod 2 < 2 by NAT_D:def 2;

reconsider j = j as Element of NAT by ORDINAL1:def 12;

(2 * (j + 1)) -' 1 = (2 * (j + 1)) - 1 by A118, A130, A131, NAT_D:39;

then g1 . i = f /. (j + 1) by A24, A25, A115, A130, A131;

then A132: |.((g1 /. i) - (f /. (j + 1))).| = |.(0. (TOP-REAL 2)).| by A119, RLVECT_1:5

.= 0 by TOPRNS_1:23 ;

((2 * j) + 1) + 1 <= ((2 * (len f)) - 1) + 1 by A33, A50, A117, A130, A131, XREAL_1:6;

then (2 * j) + 1 < 2 * (len f) by NAT_1:13;

then 2 * j < 2 * (len f) by NAT_1:13;

then (2 * j) / 2 < (2 * (len f)) / 2 by XREAL_1:74;

then A133: j + 1 <= len f by NAT_1:13;

1 <= j + 1 by NAT_1:11;

then j + 1 in dom f by A133, FINSEQ_3:25;

hence ex k being Nat st

( k in dom f & |.((g1 /. i) - (f /. k)).| < a ) by A4, A132; :: thesis: verum

then g1 . (len g1) = f . (len f) by A25, A33, A6;

hence ex g being FinSequence of (TOP-REAL 2) st

( g is special & g . 1 = f . 1 & g . (len g) = f . (len f) & len g >= len f & X_axis g lies_between (X_axis f) . 1,(X_axis f) . (len f) & Y_axis g lies_between c,d & ( for j being Nat st j in dom g holds

ex k being Nat st

( k in dom f & |.((g /. j) - (f /. k)).| < a ) ) & ( for j being Nat st 1 <= j & j + 1 <= len g holds

|.((g /. j) - (g /. (j + 1))).| < a ) ) by A1, A33, A48, A50, A89, A86, A85, A67, A114, A90, FINSEQ_4:15; :: thesis: verum