let f be FinSequence of (TOP-REAL 2); :: thesis:
let a, c, d be Real; :: thesis:
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:
A6: f . (len f) = f /. (len f) by A1, FINSEQ_4:15;
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 ) );
A7: for k being Nat st k in Seg ((2 * (len f)) -' 1) holds
ex x being object st S₁[k,x]

let k be Nat; :: thesis:
assume A8: k in Seg ((2 * (len f)) -' 1) ; :: thesis:
then A9: 1 <= k by FINSEQ_1:1;

per cases by NAT_D:12;

suppose A10: k mod 2 = 0 ; :: thesis:

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

proof

let j be Nat; :: thesis:
assume ( k = 2 * j or k = (2 * j) -' 1 ) ; :: thesis:

now :: thesis:

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

now :: thesis:

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

end;

then A14: j >= 0 + 1 by NAT_1:13;
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:

end;

end;

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

end;

suppose A15: k mod 2 = 1 ; :: thesis:

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

proof

let j be Nat; :: thesis:
assume A18: ( k = 2 * j or k = (2 * j) -' 1 ) ; :: thesis:

per cases by A18;

suppose A19: k = (2 * j) -' 1 ; :: thesis:

A20: now :: thesis:

assume k = (2 * j) -' 1 ; :: thesis:
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:

end;

k = (2 * j) - 1 by A9, A19, 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 A20; :: thesis:

end;

suppose A21: k = 2 * j ; :: thesis:

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:

end;

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

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

proof

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume y in rng p ; :: thesis:
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 by NAT_D:12;

suppose A29: i mod 2 = 0 ; :: thesis:

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:

end;

suppose A31: i mod 2 = 1 ; :: thesis:

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:

end;

then reconsider g1 = p as FinSequence of (TOP-REAL 2) by FINSEQ_1:def 4;
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

let i be Nat; :: thesis:
assume that
A34: 1 <= i and
A35: i + 1 <= len g1 ; :: thesis:
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 by NAT_D:12;

suppose A42: i mod 2 = 0 ; :: thesis:

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; :: thesis:

end;

suppose A45: i mod 2 = 1 ; :: thesis:

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; :: thesis:

end;

then A48: g1 is special by TOPREAL1:def 5;
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

let i be Nat; :: thesis:
A51: len (Y_axis f) = len f by GOBOARD1:def 2;
assume A52: i in dom (Y_axis g1) ; :: thesis:
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 by NAT_D:12;

suppose A59: i mod 2 = 0 ; :: thesis:

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

end;

suppose A63: i mod 2 = 1 ; :: thesis:

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:

end;

then A67: Y_axis g1 lies_between c,d by GOBOARD4:def 2;
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

let i be Nat; :: thesis:
A68: len (X_axis f) = len f by GOBOARD1:def 1;
assume A69: i in dom (X_axis g1) ; :: thesis:
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 by NAT_D:12;

suppose A76: i mod 2 = 0 ; :: thesis:

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

end;

suppose A81: i mod 2 = 1 ; :: thesis:

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:

end;

then A85: X_axis g1 lies_between (X_axis f) . 1,(X_axis f) . (len f) by GOBOARD4:def 2;
(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

let i be Nat; :: thesis:
assume that
A91: 1 <= i and
A92: i + 1 <= len g1 ; :: thesis:
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 by NAT_D:12;

suppose A97: i mod 2 = 0 ; :: thesis:

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;
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, A101 ;
(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
.= 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:

end;

suppose A106: i mod 2 = 1 ; :: thesis:

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;
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, A108 ;
(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 ;
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:

end;

A114: 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:
assume A115: i in dom g1 ; :: thesis:
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 by NAT_D:12;

suppose A120: i mod 2 = 0 ; :: thesis:

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;
A125: (g1 /. i) `2 = (f /. (j + 1)) `2 by A119, A123;
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) ;
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
.= 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:

end;

suppose A130: i mod 2 = 1 ; :: thesis:

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:

end;

(2 * (len f)) -' 1 in Seg ((2 * (len f)) -' 1) by A50, A88, FINSEQ_1:1;
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: