A1: (2 * 1) -' 1 = (1 + 1) -' 1
.= 1 by NAT_D:34 ;
let f be FinSequence of (TOP-REAL 2); :: thesis: for a, c, d being Real st 1 <= len f & Y_axis f lies_between (Y_axis f) . 1,(Y_axis f) . (len f) & X_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 & Y_axis g lies_between (Y_axis f) . 1,(Y_axis f) . (len f) & X_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 & Y_axis f lies_between (Y_axis f) . 1,(Y_axis f) . (len f) & X_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 & Y_axis g lies_between (Y_axis f) . 1,(Y_axis f) . (len f) & X_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
A2: 1 <= len f and
A3: Y_axis f lies_between (Y_axis f) . 1,(Y_axis f) . (len f) and
A4: X_axis f lies_between c,d and
A5: a > 0 and
A6: 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 & Y_axis g lies_between (Y_axis f) . 1,(Y_axis f) . (len f) & X_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 ) )
(len f) + (len f) >= (len f) + 1 by A2, XREAL_1:6;
then A7: (2 * (len f)) - 1 >= ((len f) + 1) - 1 by XREAL_1:9;
defpred S₁[ 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 ) );
A8: for k being Nat st k in Seg ((2 * (len f)) -' 1) holds
ex x being object st S₁[k,x]

proof

let k be Nat; :: thesis: ( k in Seg ((2 * (len f)) -' 1) implies ex x being object st S₁[k,x] )
assume A9: k in Seg ((2 * (len f)) -' 1) ; :: thesis: ex x being object st S₁[k,x]
then A10: 1 <= k by FINSEQ_1:1;

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

suppose A11: k mod 2 = 0 ; :: thesis: ex x being object st S₁[k,x]

consider i being Nat such that
A12: 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

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

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

assume A13: k = (2 * j) -' 1 ; :: thesis: contradiction

now :: thesis: not j = 0

0 - 1 < 0 ;
then A14: 0 -' 1 = 0 by XREAL_0:def 2;
assume j = 0 ; :: thesis: contradiction
hence contradiction by A9, A13, A14, FINSEQ_1:1; :: thesis: verum

end;

then A15: j >= 0 + 1 by NAT_1:13;
k = ((2 * (j - 1)) + (1 + 1)) - 1 by A10, A13, NAT_D:39
.= (2 * (j - 1)) + 1 ;
then k = (2 * (j -' 1)) + 1 by A15, XREAL_1:233;
hence contradiction by A11, NAT_D:def 2; :: thesis: verum

end;

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 A11, A12; :: thesis: verum

end;

hence ex x being object st S₁[k,x] ; :: thesis: verum

end;

suppose A16: k mod 2 = 1 ; :: thesis: ex x being object st S₁[k,x]

consider i being Nat such that
A17: k = (2 * i) + (k mod 2) and
A18: 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

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 A19: ( 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 A19;

suppose A20: 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 ) )

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

assume k = (2 * j) -' 1 ; :: thesis: f /. (i + 1) = f /. j
then k = ((2 * (j - 1)) + (1 + 1)) - 1 by A10, NAT_D:39
.= (2 * (j - 1)) + 1 ;
hence f /. (i + 1) = f /. j by A16, A17; :: thesis: verum

end;

k = (2 * j) - 1 by A10, A20, NAT_D:39;
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 A21; :: thesis: verum

end;

suppose A22: 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 A23: 2 * (j - i) = 1 by A16, A17;
then j - i >= 0 ;
then A24: j - i = j -' i by XREAL_0:def 2;
( j - i = 0 or j - i > 0 ) by A23;
then j - i >= 0 + 1 by A16, A17, A22, A24, 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 A17, A18, A22; :: thesis: verum

end;

end;

end;

hence ex x being object st S₁[k,x] ; :: thesis: verum

end;

end;

end;

ex p being FinSequence st
( dom p = Seg ((2 * (len f)) -' 1) & ( for k being Nat st k in Seg ((2 * (len f)) -' 1) holds
S₁[k,p . k] ) ) from FINSEQ_1:sch 1(A8);
then consider p being FinSequence such that
A25: dom p = Seg ((2 * (len f)) -' 1) and
A26: 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

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
A27: x in dom p and
A28: y = p . x by FUNCT_1:def 3;
reconsider i = x as Element of NAT by A27;
x in Seg (len p) by A27, FINSEQ_1:def 3;
then A29: 1 <= i by FINSEQ_1:1;

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

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

consider j being Nat such that
A31: 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 A25, A26, A27, A30, A31;
hence y in the carrier of (TOP-REAL 2) by A28; :: thesis: verum

end;

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

consider j being Nat such that
A33: 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 A29, A32, A33, NAT_D:39;
then p . i = f /. (j + 1) by A25, A26, A27, A32, A33;
hence y in the carrier of (TOP-REAL 2) by A28; :: thesis: verum

end;

end;

end;

then reconsider g1 = p as FinSequence of (TOP-REAL 2) by FINSEQ_1:def 4;
A34: len p = (2 * (len f)) -' 1 by A25, 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

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
A35: 1 <= i and
A36: i + 1 <= len g1 ; :: thesis: ( (g1 /. i) `1 = (g1 /. (i + 1)) `1 or (g1 /. i) `2 = (g1 /. (i + 1)) `2 )
1 < i + 1 by A35, NAT_1:13;
then A37: ( i + 1 in Seg (len g1) & g1 /. (i + 1) = g1 . (i + 1) ) by A36, FINSEQ_1:1, FINSEQ_4:15;
i < len g1 by A36, NAT_1:13;
then A38: ( i in Seg ((2 * (len f)) -' 1) & g1 . i = g1 /. i ) by A34, A35, FINSEQ_1:1, FINSEQ_4:15;

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

suppose A39: 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
A40: 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 A39, A40, NAT_D:39;
then A41: g1 /. (i + 1) = f /. (j + 1) by A26, A34, A37, A39, A40;
g1 /. i = |[((f /. j) `1),((f /. (j + 1)) `2)]| by A26, A38, A39, A40;
hence ( (g1 /. i) `1 = (g1 /. (i + 1)) `1 or (g1 /. i) `2 = (g1 /. (i + 1)) `2 ) by A41; :: thesis: verum

end;

suppose A42: 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
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;
i + 1 = 2 * (j + 1) by A42, A43;
then A44: g1 /. (i + 1) = |[((f /. (j + 1)) `1),((f /. ((j + 1) + 1)) `2)]| by A26, A34, A37;
(2 * (j + 1)) -' 1 = (2 * (j + 1)) - 1 by A35, A42, A43, NAT_D:39;
then g1 /. i = f /. (j + 1) by A26, A38, A42, A43;
hence ( (g1 /. i) `1 = (g1 /. (i + 1)) `1 or (g1 /. i) `2 = (g1 /. (i + 1)) `2 ) by A44; :: thesis: verum

end;

end;

end;

then A45: g1 is special by TOPREAL1:def 5;
A46: 2 * (len f) >= 2 * 1 by A2, XREAL_1:64;
then A47: (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
( (Y_axis f) . 1 <= (Y_axis g1) . i & (Y_axis g1) . i <= (Y_axis f) . (len f) )

proof

let i be Nat; :: thesis: ( i in dom (Y_axis g1) implies ( (Y_axis f) . 1 <= (Y_axis g1) . i & (Y_axis g1) . i <= (Y_axis f) . (len f) ) )
A48: len (Y_axis f) = len f by GOBOARD1:def 2;
assume A49: i in dom (Y_axis g1) ; :: thesis: ( (Y_axis f) . 1 <= (Y_axis g1) . i & (Y_axis g1) . i <= (Y_axis f) . (len f) )
then A50: i in Seg (len (Y_axis g1)) by FINSEQ_1:def 3;
then A51: i in Seg (len g1) by GOBOARD1:def 2;
i in Seg (len g1) by A50, GOBOARD1:def 2;
then A52: i <= len g1 by FINSEQ_1:1;
A53: 1 <= i by A50, FINSEQ_1:1;
then A54: g1 /. i = g1 . i by A52, FINSEQ_4:15;
A55: (Y_axis g1) . i = (g1 /. i) `2 by A49, GOBOARD1:def 2;

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

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

consider j being Nat such that
A57: 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 A26, A34, A51, A54, A56, A57;
then A58: (g1 /. i) `2 = (f /. (j + 1)) `2 ;
(2 * j) + 1 <= ((2 * (len f)) - 1) + 1 by A34, A47, A52, A56, A57, 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 A59: j + 1 in dom (Y_axis f) by A48, FINSEQ_1:def 3;
then (Y_axis f) . (j + 1) = (f /. (j + 1)) `2 by GOBOARD1:def 2;
hence ( (Y_axis f) . 1 <= (Y_axis g1) . i & (Y_axis g1) . i <= (Y_axis f) . (len f) ) by A3, A55, A58, A59, GOBOARD4:def 2; :: thesis: verum

end;

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

consider j being Nat such that
A61: 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 A53, A60, A61, NAT_D:39;
then A62: (g1 /. i) `2 = (f /. (j + 1)) `2 by A26, A34, A51, A54, A60, A61;
(2 * j) + 1 <= ((2 * (len f)) - 1) + 1 by A34, A47, A52, A60, A61, 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 A63: j + 1 in dom (Y_axis f) by A48, FINSEQ_1:def 3;
then (Y_axis f) . (j + 1) = (f /. (j + 1)) `2 by GOBOARD1:def 2;
hence ( (Y_axis f) . 1 <= (Y_axis g1) . i & (Y_axis g1) . i <= (Y_axis f) . (len f) ) by A3, A55, A62, A63, GOBOARD4:def 2; :: thesis: verum

end;

end;

end;

then A64: Y_axis g1 lies_between (Y_axis f) . 1,(Y_axis f) . (len f) by GOBOARD4:def 2;
A65: (2 * (len f)) - 1 >= (1 + 1) - 1 by A46, XREAL_1:9;
then 1 in Seg ((2 * (len f)) -' 1) by A47, FINSEQ_1:1;
then p . 1 = f /. 1 by A26, A1;
then A66: g1 . 1 = f . 1 by A2, FINSEQ_4:15;
A67: for i being Nat st 1 <= i & i + 1 <= len g1 holds
|.((g1 /. i) - (g1 /. (i + 1))).| < a

proof

let i be Nat; :: thesis: ( 1 <= i & i + 1 <= len g1 implies |.((g1 /. i) - (g1 /. (i + 1))).| < a )
assume that
A68: 1 <= i and
A69: i + 1 <= len g1 ; :: thesis: |.((g1 /. i) - (g1 /. (i + 1))).| < a
A70: g1 . (i + 1) = g1 /. (i + 1) by A69, FINSEQ_4:15, NAT_1:11;
i <= len g1 by A69, NAT_1:13;
then A71: i in Seg (len g1) by A68, FINSEQ_1:1;
1 <= i + 1 by NAT_1:11;
then A72: i + 1 in Seg ((2 * (len f)) -' 1) by A34, A69, FINSEQ_1:1;
i <= len g1 by A69, NAT_1:13;
then A73: g1 . i = g1 /. i by A68, FINSEQ_4:15;

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

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

consider j being Nat such that
A75: 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;
A76: g1 /. i = |[((f /. j) `1),((f /. (j + 1)) `2)]| by A26, A34, A71, A73, A74, A75;
1 <= 1 + i by NAT_1:11;
then (2 * (j + 1)) -' 1 = (2 * (j + 1)) - 1 by A74, A75, NAT_D:39;
then A78: g1 /. (i + 1) = f /. (j + 1) by A26, A72, A70, A74, A75;
(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 A76, A78 ;
then ( ((g1 /. i) - (g1 /. (i + 1))) `1 = ((f /. j) `1) - ((f /. (j + 1)) `1) & ((g1 /. i) - (g1 /. (i + 1))) `2 = 0 ) ;
then |.((g1 /. i) - (g1 /. (i + 1))).| = sqrt (((((f /. j) `1) - ((f /. (j + 1)) `1)) ^2) + (0 ^2)) by Th30
.= 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 A79: |.((g1 /. i) - (g1 /. (i + 1))).| <= |.((f /. j) - (f /. (j + 1))).| by Th34;
(2 * j) + 1 <= ((2 * (len f)) - 1) + 1 by A34, A47, A69, A74, A75, 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 A80: j + 1 <= len f by NAT_1:13;
j > 0 by A68, A74, A75;
then j >= 0 + 1 by NAT_1:13;
then |.((f /. j) - (f /. (j + 1))).| < a by A6, A80;
hence |.((g1 /. i) - (g1 /. (i + 1))).| < a by A79, XXREAL_0:2; :: thesis: verum

end;

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

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 A68, A81, A82, NAT_D:39;
then A83: g1 /. i = f /. (j + 1) by A26, A34, A71, A73, A81, A82;
i + 1 = 2 * (j + 1) by A81, A82;
then A84: g1 /. (i + 1) = |[((f /. (j + 1)) `1),((f /. ((j + 1) + 1)) `2)]| by A26, A72, A70;
(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 A83, A84 ;
then ( ((g1 /. i) - (g1 /. (i + 1))) `1 = 0 & ((g1 /. i) - (g1 /. (i + 1))) `2 = ((f /. (j + 1)) `2) - ((f /. ((j + 1) + 1)) `2) ) ;
then |.((g1 /. i) - (g1 /. (i + 1))).| = sqrt ((0 ^2) + ((((f /. (j + 1)) `2) - ((f /. ((j + 1) + 1)) `2)) ^2)) by Th30
.= sqrt ((((f /. (j + 1)) `2) - ((f /. ((j + 1) + 1)) `2)) ^2) ;
then |.((g1 /. i) - (g1 /. (i + 1))).| = |.(((f /. (j + 1)) `2) - ((f /. ((j + 1) + 1)) `2)).| by COMPLEX1:72;
then A86: |.((g1 /. i) - (g1 /. (i + 1))).| <= |.((f /. (j + 1)) - (f /. ((j + 1) + 1))).| by Th34;
(2 * (j + 1)) + 1 <= ((2 * (len f)) - 1) + 1 by A34, A47, A69, A81, A82, 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 |.((f /. (j + 1)) - (f /. ((j + 1) + 1))).| < a by A6, NAT_1:11;
hence |.((g1 /. i) - (g1 /. (i + 1))).| < a by A86, XXREAL_0:2; :: thesis: verum

end;

end;

end;

A87: for i being Nat st i in dom g1 holds
ex k being Nat st
( k in dom f & |.((g1 /. i) - (f /. k)).| < a )

proof

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 A88: i in dom g1 ; :: thesis: ex k being Nat st
( k in dom f & |.((g1 /. i) - (f /. k)).| < a )
then A89: i <= len g1 by FINSEQ_3:25;
A90: 1 <= i by A88, FINSEQ_3:25;
then A91: g1 . i = g1 /. i by A89, FINSEQ_4:15;

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

suppose A92: i mod 2 = 0 ; :: thesis: ex k being Nat st
( k in dom f & |.((g1 /. i) - (f /. k)).| < a )

consider j being Nat such that
A93: 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 A88, A92, A93, FINSEQ_3:25;
then A94: j >= 0 + 1 by NAT_1:13;
A95: g1 /. i = |[((f /. j) `1),((f /. (j + 1)) `2)]| by A25, A26, A88, A91, A92, A93;
then A96: (g1 /. i) `1 = (f /. j) `1 ;
A97: (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 A96 ;
then A98: ((g1 /. i) - (f /. j)) `1 = 0 ;
((g1 /. i) - (f /. j)) `2 = ((g1 /. i) `2) - ((f /. j) `2) by A97;
then |.((g1 /. i) - (f /. j)).| = sqrt (((((g1 /. i) - (f /. j)) `1) ^2) + ((((g1 /. i) `2) - ((f /. j) `2)) ^2)) by Th30
.= sqrt ((((f /. (j + 1)) `2) - ((f /. j) `2)) ^2) by A95, A98 ;
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 A99: |.((g1 /. i) - (f /. j)).| <= |.((f /. j) - (f /. (j + 1))).| by Th34;
(2 * j) + 1 <= ((2 * (len f)) - 1) + 1 by A34, A47, A89, A92, A93, XREAL_1:6;
then 2 * j < 2 * (len f) by NAT_1:13;
then A100: (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 A6, A94;
then A101: |.((g1 /. i) - (f /. j)).| < a by A99, XXREAL_0:2;
j in dom f by A94, A100, FINSEQ_3:25;
hence ex k being Nat st
( k in dom f & |.((g1 /. i) - (f /. k)).| < a ) by A101; :: thesis: verum

end;

suppose A102: i mod 2 = 1 ; :: thesis: ex k being Nat st
( k in dom f & |.((g1 /. i) - (f /. k)).| < a )

consider j being Nat such that
A103: 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 A90, A102, A103, NAT_D:39;
then g1 /. i = f /. (j + 1) by A25, A26, A88, A91, A102, A103;
then A104: |.((g1 /. i) - (f /. (j + 1))).| = |.(0. (TOP-REAL 2)).| by RLVECT_1:5
.= 0 by TOPRNS_1:23 ;
((2 * j) + 1) + 1 <= ((2 * (len f)) - 1) + 1 by A34, A47, A89, A102, A103, 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 A105: j + 1 <= len f by NAT_1:13;
1 <= j + 1 by NAT_1:11;
then j + 1 in dom f by A105, FINSEQ_3:25;
hence ex k being Nat st
( k in dom f & |.((g1 /. i) - (f /. k)).| < a ) by A5, A104; :: thesis: verum

end;

end;

end;

for i being Nat st i in dom (X_axis g1) holds
( c <= (X_axis g1) . i & (X_axis g1) . i <= d )

proof

let i be Nat; :: thesis: ( i in dom (X_axis g1) implies ( c <= (X_axis g1) . i & (X_axis g1) . i <= d ) )
A106: len (X_axis f) = len f by GOBOARD1:def 1;
assume A107: i in dom (X_axis g1) ; :: thesis: ( c <= (X_axis g1) . i & (X_axis g1) . i <= d )
then A108: i in Seg (len (X_axis g1)) by FINSEQ_1:def 3;
then A109: i in Seg (len g1) by GOBOARD1:def 1;
then A110: i <= len g1 by FINSEQ_1:1;
A111: 1 <= i by A108, FINSEQ_1:1;
then A112: g1 /. i = g1 . i by A110, FINSEQ_4:15;
A113: (X_axis g1) . i = (g1 /. i) `1 by A107, GOBOARD1:def 1;

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

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

consider j being Nat such that
A115: 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 A26, A34, A109, A112, A114, A115;
then A116: (g1 /. i) `1 = (f /. j) `1 ;
(2 * j) + 1 <= ((2 * (len f)) - 1) + 1 by A34, A47, A110, A114, A115, XREAL_1:6;
then 2 * j < 2 * (len f) by NAT_1:13;
then A117: (2 * j) / 2 < (2 * (len f)) / 2 by XREAL_1:74;
j > 0 by A108, A114, A115, FINSEQ_1:1;
then j >= 0 + 1 by NAT_1:13;
then j in Seg (len f) by A117, FINSEQ_1:1;
then A118: j in dom (X_axis f) by A106, FINSEQ_1:def 3;
then (X_axis f) . j = (f /. j) `1 by GOBOARD1:def 1;
hence ( c <= (X_axis g1) . i & (X_axis g1) . i <= d ) by A4, A113, A116, A118, GOBOARD4:def 2; :: thesis: verum

end;

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

consider j being Nat such that
A120: 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 A111, A119, A120, NAT_D:39;
then A121: (g1 /. i) `1 = (f /. (j + 1)) `1 by A26, A34, A109, A112, A119, A120;
(2 * j) + 1 <= ((2 * (len f)) - 1) + 1 by A34, A47, A110, A119, A120, 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 A122: j + 1 in dom (X_axis f) by A106, FINSEQ_1:def 3;
then (X_axis f) . (j + 1) = (f /. (j + 1)) `1 by GOBOARD1:def 1;
hence ( c <= (X_axis g1) . i & (X_axis g1) . i <= d ) by A4, A113, A121, A122, GOBOARD4:def 2; :: thesis: verum

end;

end;

end;

then A123: X_axis g1 lies_between c,d by GOBOARD4:def 2;
(2 * (len f)) -' 1 in Seg ((2 * (len f)) -' 1) by A47, A65, FINSEQ_1:1;
then p . ((2 * (len f)) -' 1) = f /. (len f) by A26;
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 & Y_axis g lies_between (Y_axis f) . 1,(Y_axis f) . (len f) & X_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 A2, A34, A45, A47, A66, A7, A64, A123, A87, A67, FINSEQ_4:15; :: thesis: verum