let f be V8() standard special_circular_sequence; :: thesis: ex i being Nat st

( i in dom f & (f /. i) `1 <> (f /. 1) `1 )

assume A1: for i being Nat st i in dom f holds

(f /. i) `1 = (f /. 1) `1 ; :: thesis: contradiction

A2: len f > 1 by Lm2;

then A3: len f >= 1 + 1 by NAT_1:13;

then A4: 1 + 1 in dom f by FINSEQ_3:25;

then A7: 2 < len f by A3, A5, XXREAL_0:1;

( i in dom f & (f /. i) `1 <> (f /. 1) `1 )

assume A1: for i being Nat st i in dom f holds

(f /. i) `1 = (f /. 1) `1 ; :: thesis: contradiction

A2: len f > 1 by Lm2;

then A3: len f >= 1 + 1 by NAT_1:13;

then A4: 1 + 1 in dom f by FINSEQ_3:25;

A5: now :: thesis: not (f /. 2) `2 = (f /. 1) `2

( len f = 2 implies f /. 2 = f /. 1 )
by FINSEQ_6:def 1;assume A6:
(f /. 2) `2 = (f /. 1) `2
; :: thesis: contradiction

(f /. 2) `1 = (f /. 1) `1 by A1, A4;

then f /. 2 = |[((f /. 1) `1),((f /. 1) `2)]| by A6, EUCLID:53

.= f /. 1 by EUCLID:53 ;

hence contradiction by A4, Th29, FINSEQ_5:6; :: thesis: verum

end;(f /. 2) `1 = (f /. 1) `1 by A1, A4;

then f /. 2 = |[((f /. 1) `1),((f /. 1) `2)]| by A6, EUCLID:53

.= f /. 1 by EUCLID:53 ;

hence contradiction by A4, Th29, FINSEQ_5:6; :: thesis: verum

then A7: 2 < len f by A3, A5, XXREAL_0:1;

per cases
( (f /. 2) `2 < (f /. 1) `2 or (f /. 2) `2 > (f /. 1) `2 )
by A5, XXREAL_0:1;

end;

suppose A8:
(f /. 2) `2 < (f /. 1) `2
; :: thesis: contradiction

defpred S_{1}[ Nat] means ( 2 <= $1 & $1 < len f implies ( (f /. $1) `2 <= (f /. 2) `2 & (f /. ($1 + 1)) `2 < (f /. $1) `2 ) );

A9: for j being Nat st S_{1}[j] holds

S_{1}[j + 1]

then A31: ( 2 <= (len f) -' 1 & (len f) -' 1 < len f ) by A7, NAT_1:13;

A32: S_{1}[ 0 ]
;

A33: for j being Nat holds S_{1}[j]
from NAT_1:sch 2(A32, A9);

then A34: (f /. ((len f) -' 1)) `2 <= (f /. 2) `2 by A31;

(f /. (len f)) `2 < (f /. ((len f) -' 1)) `2 by A33, A30, A31;

then (f /. (len f)) `2 < (f /. 2) `2 by A34, XXREAL_0:2;

hence contradiction by A8, FINSEQ_6:def 1; :: thesis: verum

end;A9: for j being Nat st S

S

proof

A30:
((len f) -' 1) + 1 = len f
by A2, XREAL_1:235;
let j be Nat; :: thesis: ( S_{1}[j] implies S_{1}[j + 1] )

assume that

A10: ( 2 <= j & j < len f implies ( (f /. j) `2 <= (f /. 2) `2 & (f /. (j + 1)) `2 < (f /. j) `2 ) ) and

A11: 2 <= j + 1 and

A12: j + 1 < len f ; :: thesis: ( (f /. (j + 1)) `2 <= (f /. 2) `2 & (f /. ((j + 1) + 1)) `2 < (f /. (j + 1)) `2 )

1 + 1 <= j + 1 by A11;

then A13: 1 <= j by XREAL_1:6;

thus (f /. (j + 1)) `2 <= (f /. 2) `2 :: thesis: (f /. ((j + 1) + 1)) `2 < (f /. (j + 1)) `2

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

then A18: (f /. (j + 1)) `1 = (f /. 1) `1 by A1;

j < len f by A12, NAT_1:13;

then A19: j in dom f by A13, FINSEQ_3:25;

then A20: (f /. j) `1 = (f /. 1) `1 by A1;

1 <= (j + 1) + 1 by NAT_1:11;

then A21: (j + 1) + 1 in dom f by A14, FINSEQ_3:25;

then A22: (f /. ((j + 1) + 1)) `1 = (f /. 1) `1 by A1;

assume A23: (f /. ((j + 1) + 1)) `2 >= (f /. (j + 1)) `2 ; :: thesis: contradiction

end;assume that

A10: ( 2 <= j & j < len f implies ( (f /. j) `2 <= (f /. 2) `2 & (f /. (j + 1)) `2 < (f /. j) `2 ) ) and

A11: 2 <= j + 1 and

A12: j + 1 < len f ; :: thesis: ( (f /. (j + 1)) `2 <= (f /. 2) `2 & (f /. ((j + 1) + 1)) `2 < (f /. (j + 1)) `2 )

1 + 1 <= j + 1 by A11;

then A13: 1 <= j by XREAL_1:6;

thus (f /. (j + 1)) `2 <= (f /. 2) `2 :: thesis: (f /. ((j + 1) + 1)) `2 < (f /. (j + 1)) `2

proof
end;

A14:
(j + 1) + 1 <= len f
by A12, NAT_1:13;A15: now :: thesis: (f /. (j + 1)) `2 < (f /. j) `2

A16:
1 <= j + 1
by NAT_1:11;end;

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

then A18: (f /. (j + 1)) `1 = (f /. 1) `1 by A1;

j < len f by A12, NAT_1:13;

then A19: j in dom f by A13, FINSEQ_3:25;

then A20: (f /. j) `1 = (f /. 1) `1 by A1;

1 <= (j + 1) + 1 by NAT_1:11;

then A21: (j + 1) + 1 in dom f by A14, FINSEQ_3:25;

then A22: (f /. ((j + 1) + 1)) `1 = (f /. 1) `1 by A1;

assume A23: (f /. ((j + 1) + 1)) `2 >= (f /. (j + 1)) `2 ; :: thesis: contradiction

per cases
( (f /. ((j + 1) + 1)) `2 > (f /. (j + 1)) `2 or (f /. ((j + 1) + 1)) `2 = (f /. (j + 1)) `2 )
by A23, XXREAL_0:1;

end;

suppose A24:
(f /. ((j + 1) + 1)) `2 > (f /. (j + 1)) `2
; :: thesis: contradiction

end;

now :: thesis: contradictionend;

hence
contradiction
; :: thesis: verumper cases
( (f /. j) `2 <= (f /. ((j + 1) + 1)) `2 or (f /. j) `2 >= (f /. ((j + 1) + 1)) `2 )
;

end;

suppose
(f /. j) `2 <= (f /. ((j + 1) + 1)) `2
; :: thesis: contradiction

then
f /. j in LSeg ((f /. (j + 1)),(f /. ((j + 1) + 1)))
by A15, A20, A18, A22, Th7;

then A25: f /. j in LSeg (f,(j + 1)) by A14, A16, TOPREAL1:def 3;

(j + 1) + 1 = j + (1 + 1) ;

then A26: (LSeg (f,j)) /\ (LSeg (f,(j + 1))) = {(f /. (j + 1))} by A14, A13, TOPREAL1:def 6;

f /. j in LSeg (f,j) by A12, A13, TOPREAL1:21;

then f /. j in (LSeg (f,j)) /\ (LSeg (f,(j + 1))) by A25, XBOOLE_0:def 4;

then f /. j = f /. (j + 1) by A26, TARSKI:def 1;

hence contradiction by A19, A17, Th29; :: thesis: verum

end;then A25: f /. j in LSeg (f,(j + 1)) by A14, A16, TOPREAL1:def 3;

(j + 1) + 1 = j + (1 + 1) ;

then A26: (LSeg (f,j)) /\ (LSeg (f,(j + 1))) = {(f /. (j + 1))} by A14, A13, TOPREAL1:def 6;

f /. j in LSeg (f,j) by A12, A13, TOPREAL1:21;

then f /. j in (LSeg (f,j)) /\ (LSeg (f,(j + 1))) by A25, XBOOLE_0:def 4;

then f /. j = f /. (j + 1) by A26, TARSKI:def 1;

hence contradiction by A19, A17, Th29; :: thesis: verum

suppose
(f /. j) `2 >= (f /. ((j + 1) + 1)) `2
; :: thesis: contradiction

then
f /. ((j + 1) + 1) in LSeg ((f /. j),(f /. (j + 1)))
by A20, A18, A22, A24, Th7;

then A27: f /. ((j + 1) + 1) in LSeg (f,j) by A12, A13, TOPREAL1:def 3;

(j + 1) + 1 = j + (1 + 1) ;

then A28: (LSeg (f,j)) /\ (LSeg (f,(j + 1))) = {(f /. (j + 1))} by A14, A13, TOPREAL1:def 6;

f /. ((j + 1) + 1) in LSeg (f,(j + 1)) by A14, A16, TOPREAL1:21;

then f /. ((j + 1) + 1) in (LSeg (f,j)) /\ (LSeg (f,(j + 1))) by A27, XBOOLE_0:def 4;

then f /. ((j + 1) + 1) = f /. (j + 1) by A28, TARSKI:def 1;

hence contradiction by A17, A21, Th29; :: thesis: verum

end;then A27: f /. ((j + 1) + 1) in LSeg (f,j) by A12, A13, TOPREAL1:def 3;

(j + 1) + 1 = j + (1 + 1) ;

then A28: (LSeg (f,j)) /\ (LSeg (f,(j + 1))) = {(f /. (j + 1))} by A14, A13, TOPREAL1:def 6;

f /. ((j + 1) + 1) in LSeg (f,(j + 1)) by A14, A16, TOPREAL1:21;

then f /. ((j + 1) + 1) in (LSeg (f,j)) /\ (LSeg (f,(j + 1))) by A27, XBOOLE_0:def 4;

then f /. ((j + 1) + 1) = f /. (j + 1) by A28, TARSKI:def 1;

hence contradiction by A17, A21, Th29; :: thesis: verum

suppose A29:
(f /. ((j + 1) + 1)) `2 = (f /. (j + 1)) `2
; :: thesis: contradiction

(f /. ((j + 1) + 1)) `1 =
(f /. 1) `1
by A1, A21

.= (f /. (j + 1)) `1 by A1, A17 ;

then f /. ((j + 1) + 1) = |[((f /. (j + 1)) `1),((f /. (j + 1)) `2)]| by A29, EUCLID:53

.= f /. (j + 1) by EUCLID:53 ;

hence contradiction by A17, A21, Th29; :: thesis: verum

end;.= (f /. (j + 1)) `1 by A1, A17 ;

then f /. ((j + 1) + 1) = |[((f /. (j + 1)) `1),((f /. (j + 1)) `2)]| by A29, EUCLID:53

.= f /. (j + 1) by EUCLID:53 ;

hence contradiction by A17, A21, Th29; :: thesis: verum

then A31: ( 2 <= (len f) -' 1 & (len f) -' 1 < len f ) by A7, NAT_1:13;

A32: S

A33: for j being Nat holds S

then A34: (f /. ((len f) -' 1)) `2 <= (f /. 2) `2 by A31;

(f /. (len f)) `2 < (f /. ((len f) -' 1)) `2 by A33, A30, A31;

then (f /. (len f)) `2 < (f /. 2) `2 by A34, XXREAL_0:2;

hence contradiction by A8, FINSEQ_6:def 1; :: thesis: verum

suppose A35:
(f /. 2) `2 > (f /. 1) `2
; :: thesis: contradiction

defpred S_{1}[ Nat] means ( 2 <= $1 & $1 < len f implies ( (f /. $1) `2 >= (f /. 2) `2 & (f /. ($1 + 1)) `2 > (f /. $1) `2 ) );

A36: for j being Nat st S_{1}[j] holds

S_{1}[j + 1]

then A58: ( 2 <= (len f) -' 1 & (len f) -' 1 < len f ) by A7, NAT_1:13;

A59: S_{1}[ 0 ]
;

A60: for j being Nat holds S_{1}[j]
from NAT_1:sch 2(A59, A36);

then A61: (f /. ((len f) -' 1)) `2 >= (f /. 2) `2 by A58;

(f /. (len f)) `2 > (f /. ((len f) -' 1)) `2 by A60, A57, A58;

then (f /. (len f)) `2 > (f /. 2) `2 by A61, XXREAL_0:2;

hence contradiction by A35, FINSEQ_6:def 1; :: thesis: verum

end;A36: for j being Nat st S

S

proof

A57:
((len f) -' 1) + 1 = len f
by A2, XREAL_1:235;
let j be Nat; :: thesis: ( S_{1}[j] implies S_{1}[j + 1] )

assume that

A37: ( 2 <= j & j < len f implies ( (f /. j) `2 >= (f /. 2) `2 & (f /. (j + 1)) `2 > (f /. j) `2 ) ) and

A38: 2 <= j + 1 and

A39: j + 1 < len f ; :: thesis: ( (f /. (j + 1)) `2 >= (f /. 2) `2 & (f /. ((j + 1) + 1)) `2 > (f /. (j + 1)) `2 )

1 + 1 <= j + 1 by A38;

then A40: 1 <= j by XREAL_1:6;

thus (f /. (j + 1)) `2 >= (f /. 2) `2 :: thesis: (f /. ((j + 1) + 1)) `2 > (f /. (j + 1)) `2

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

then A45: (f /. (j + 1)) `1 = (f /. 1) `1 by A1;

j < len f by A39, NAT_1:13;

then A46: j in dom f by A40, FINSEQ_3:25;

then A47: (f /. j) `1 = (f /. 1) `1 by A1;

1 <= (j + 1) + 1 by NAT_1:11;

then A48: (j + 1) + 1 in dom f by A41, FINSEQ_3:25;

then A49: (f /. ((j + 1) + 1)) `1 = (f /. 1) `1 by A1;

assume A50: (f /. ((j + 1) + 1)) `2 <= (f /. (j + 1)) `2 ; :: thesis: contradiction

end;assume that

A37: ( 2 <= j & j < len f implies ( (f /. j) `2 >= (f /. 2) `2 & (f /. (j + 1)) `2 > (f /. j) `2 ) ) and

A38: 2 <= j + 1 and

A39: j + 1 < len f ; :: thesis: ( (f /. (j + 1)) `2 >= (f /. 2) `2 & (f /. ((j + 1) + 1)) `2 > (f /. (j + 1)) `2 )

1 + 1 <= j + 1 by A38;

then A40: 1 <= j by XREAL_1:6;

thus (f /. (j + 1)) `2 >= (f /. 2) `2 :: thesis: (f /. ((j + 1) + 1)) `2 > (f /. (j + 1)) `2

proof
end;

A41:
(j + 1) + 1 <= len f
by A39, NAT_1:13;A42: now :: thesis: (f /. (j + 1)) `2 > (f /. j) `2

A43:
1 <= j + 1
by NAT_1:11;end;

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

then A45: (f /. (j + 1)) `1 = (f /. 1) `1 by A1;

j < len f by A39, NAT_1:13;

then A46: j in dom f by A40, FINSEQ_3:25;

then A47: (f /. j) `1 = (f /. 1) `1 by A1;

1 <= (j + 1) + 1 by NAT_1:11;

then A48: (j + 1) + 1 in dom f by A41, FINSEQ_3:25;

then A49: (f /. ((j + 1) + 1)) `1 = (f /. 1) `1 by A1;

assume A50: (f /. ((j + 1) + 1)) `2 <= (f /. (j + 1)) `2 ; :: thesis: contradiction

per cases
( (f /. ((j + 1) + 1)) `2 < (f /. (j + 1)) `2 or (f /. ((j + 1) + 1)) `2 = (f /. (j + 1)) `2 )
by A50, XXREAL_0:1;

end;

suppose A51:
(f /. ((j + 1) + 1)) `2 < (f /. (j + 1)) `2
; :: thesis: contradiction

end;

now :: thesis: contradictionend;

hence
contradiction
; :: thesis: verumper cases
( (f /. j) `2 >= (f /. ((j + 1) + 1)) `2 or (f /. j) `2 <= (f /. ((j + 1) + 1)) `2 )
;

end;

suppose
(f /. j) `2 >= (f /. ((j + 1) + 1)) `2
; :: thesis: contradiction

then
f /. j in LSeg ((f /. (j + 1)),(f /. ((j + 1) + 1)))
by A42, A47, A45, A49, Th7;

then A52: f /. j in LSeg (f,(j + 1)) by A41, A43, TOPREAL1:def 3;

(j + 1) + 1 = j + (1 + 1) ;

then A53: (LSeg (f,j)) /\ (LSeg (f,(j + 1))) = {(f /. (j + 1))} by A41, A40, TOPREAL1:def 6;

f /. j in LSeg (f,j) by A39, A40, TOPREAL1:21;

then f /. j in (LSeg (f,j)) /\ (LSeg (f,(j + 1))) by A52, XBOOLE_0:def 4;

then f /. j = f /. (j + 1) by A53, TARSKI:def 1;

hence contradiction by A46, A44, Th29; :: thesis: verum

end;then A52: f /. j in LSeg (f,(j + 1)) by A41, A43, TOPREAL1:def 3;

(j + 1) + 1 = j + (1 + 1) ;

then A53: (LSeg (f,j)) /\ (LSeg (f,(j + 1))) = {(f /. (j + 1))} by A41, A40, TOPREAL1:def 6;

f /. j in LSeg (f,j) by A39, A40, TOPREAL1:21;

then f /. j in (LSeg (f,j)) /\ (LSeg (f,(j + 1))) by A52, XBOOLE_0:def 4;

then f /. j = f /. (j + 1) by A53, TARSKI:def 1;

hence contradiction by A46, A44, Th29; :: thesis: verum

suppose
(f /. j) `2 <= (f /. ((j + 1) + 1)) `2
; :: thesis: contradiction

then
f /. ((j + 1) + 1) in LSeg ((f /. j),(f /. (j + 1)))
by A47, A45, A49, A51, Th7;

then A54: f /. ((j + 1) + 1) in LSeg (f,j) by A39, A40, TOPREAL1:def 3;

(j + 1) + 1 = j + (1 + 1) ;

then A55: (LSeg (f,j)) /\ (LSeg (f,(j + 1))) = {(f /. (j + 1))} by A41, A40, TOPREAL1:def 6;

f /. ((j + 1) + 1) in LSeg (f,(j + 1)) by A41, A43, TOPREAL1:21;

then f /. ((j + 1) + 1) in (LSeg (f,j)) /\ (LSeg (f,(j + 1))) by A54, XBOOLE_0:def 4;

then f /. ((j + 1) + 1) = f /. (j + 1) by A55, TARSKI:def 1;

hence contradiction by A44, A48, Th29; :: thesis: verum

end;then A54: f /. ((j + 1) + 1) in LSeg (f,j) by A39, A40, TOPREAL1:def 3;

(j + 1) + 1 = j + (1 + 1) ;

then A55: (LSeg (f,j)) /\ (LSeg (f,(j + 1))) = {(f /. (j + 1))} by A41, A40, TOPREAL1:def 6;

f /. ((j + 1) + 1) in LSeg (f,(j + 1)) by A41, A43, TOPREAL1:21;

then f /. ((j + 1) + 1) in (LSeg (f,j)) /\ (LSeg (f,(j + 1))) by A54, XBOOLE_0:def 4;

then f /. ((j + 1) + 1) = f /. (j + 1) by A55, TARSKI:def 1;

hence contradiction by A44, A48, Th29; :: thesis: verum

suppose A56:
(f /. ((j + 1) + 1)) `2 = (f /. (j + 1)) `2
; :: thesis: contradiction

(f /. ((j + 1) + 1)) `1 =
(f /. 1) `1
by A1, A48

.= (f /. (j + 1)) `1 by A1, A44 ;

then f /. ((j + 1) + 1) = |[((f /. (j + 1)) `1),((f /. (j + 1)) `2)]| by A56, EUCLID:53

.= f /. (j + 1) by EUCLID:53 ;

hence contradiction by A44, A48, Th29; :: thesis: verum

end;.= (f /. (j + 1)) `1 by A1, A44 ;

then f /. ((j + 1) + 1) = |[((f /. (j + 1)) `1),((f /. (j + 1)) `2)]| by A56, EUCLID:53

.= f /. (j + 1) by EUCLID:53 ;

hence contradiction by A44, A48, Th29; :: thesis: verum

then A58: ( 2 <= (len f) -' 1 & (len f) -' 1 < len f ) by A7, NAT_1:13;

A59: S

A60: for j being Nat holds S

then A61: (f /. ((len f) -' 1)) `2 >= (f /. 2) `2 by A58;

(f /. (len f)) `2 > (f /. ((len f) -' 1)) `2 by A60, A57, A58;

then (f /. (len f)) `2 > (f /. 2) `2 by A61, XXREAL_0:2;

hence contradiction by A35, FINSEQ_6:def 1; :: thesis: verum