let f be V8() standard special_circular_sequence; :: thesis: ex i being Nat st
( i in dom f & (f /. i) `2 <> (f /. 1) `2 )

assume A1: for i being Nat st i in dom f holds
(f /. i) `2 = (f /. 1) `2 ; :: 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) `1 = (f /. 1) `1
assume A6: (f /. 2) `1 = (f /. 1) `1 ; :: thesis: contradiction
(f /. 2) `2 = (f /. 1) `2 by A1, A4;
then f /. 2 = |[((f /. 1) `1),((f /. 1) `2)]| by
.= f /. 1 by EUCLID:53 ;
hence contradiction by A4, Th29, FINSEQ_5:6; :: thesis: verum
end;
( len f = 2 implies f /. 2 = f /. 1 ) by FINSEQ_6:def 1;
then A7: 2 < len f by ;
per cases ) `1 < (f /. 1) `1 or (f /. 2) `1 > (f /. 1) `1 ) by ;
suppose A8: (f /. 2) `1 < (f /. 1) `1 ; :: thesis: contradiction
defpred S1[ Nat] means ( 2 <= \$1 & \$1 < len f implies ( (f /. \$1) `1 <= (f /. 2) `1 & (f /. (\$1 + 1)) `1 < (f /. \$1) `1 ) );
A9: for j being Nat st S1[j] holds
S1[j + 1]
proof
let j be Nat; :: thesis: ( S1[j] implies S1[j + 1] )
assume that
A10: ( 2 <= j & j < len f implies ( (f /. j) `1 <= (f /. 2) `1 & (f /. (j + 1)) `1 < (f /. j) `1 ) ) and
A11: 2 <= j + 1 and
A12: j + 1 < len f ; :: thesis: ( (f /. (j + 1)) `1 <= (f /. 2) `1 & (f /. ((j + 1) + 1)) `1 < (f /. (j + 1)) `1 )
1 + 1 <= j + 1 by A11;
then A13: 1 <= j by XREAL_1:6;
thus (f /. (j + 1)) `1 <= (f /. 2) `1 :: thesis: (f /. ((j + 1) + 1)) `1 < (f /. (j + 1)) `1
proof
per cases ( 2 = j + 1 or 2 < j + 1 ) by ;
suppose 2 = j + 1 ; :: thesis: (f /. (j + 1)) `1 <= (f /. 2) `1
hence (f /. (j + 1)) `1 <= (f /. 2) `1 ; :: thesis: verum
end;
suppose 2 < j + 1 ; :: thesis: (f /. (j + 1)) `1 <= (f /. 2) `1
hence (f /. (j + 1)) `1 <= (f /. 2) `1 by ; :: thesis: verum
end;
end;
end;
A14: (j + 1) + 1 <= len f by ;
A15: now :: thesis: (f /. (j + 1)) `1 < (f /. j) `1
per cases ( 1 + 1 = j + 1 or 2 < j + 1 ) by ;
suppose 1 + 1 = j + 1 ; :: thesis: (f /. (j + 1)) `1 < (f /. j) `1
hence (f /. (j + 1)) `1 < (f /. j) `1 by A8; :: thesis: verum
end;
suppose 2 < j + 1 ; :: thesis: (f /. (j + 1)) `1 < (f /. j) `1
hence (f /. (j + 1)) `1 < (f /. j) `1 by ; :: thesis: verum
end;
end;
end;
A16: 1 <= j + 1 by NAT_1:11;
then A17: j + 1 in dom f by ;
then A18: (f /. (j + 1)) `2 = (f /. 1) `2 by A1;
j < len f by ;
then A19: j in dom f by ;
then A20: (f /. j) `2 = (f /. 1) `2 by A1;
1 <= (j + 1) + 1 by NAT_1:11;
then A21: (j + 1) + 1 in dom f by ;
then A22: (f /. ((j + 1) + 1)) `2 = (f /. 1) `2 by A1;
assume A23: (f /. ((j + 1) + 1)) `1 >= (f /. (j + 1)) `1 ; :: thesis: contradiction
per cases ( (f /. ((j + 1) + 1)) `1 > (f /. (j + 1)) `1 or (f /. ((j + 1) + 1)) `1 = (f /. (j + 1)) `1 ) by ;
suppose A24: (f /. ((j + 1) + 1)) `1 > (f /. (j + 1)) `1 ; :: thesis: contradiction
per cases ) `1 <= (f /. ((j + 1) + 1)) `1 or (f /. j) `1 >= (f /. ((j + 1) + 1)) `1 ) ;
suppose (f /. j) `1 <= (f /. ((j + 1) + 1)) `1 ; :: thesis: contradiction
then f /. j in LSeg ((f /. (j + 1)),(f /. ((j + 1) + 1))) by A15, A20, A18, A22, Th8;
then A25: f /. j in LSeg (f,(j + 1)) by ;
(j + 1) + 1 = j + (1 + 1) ;
then A26: (LSeg (f,j)) /\ (LSeg (f,(j + 1))) = {(f /. (j + 1))} by ;
f /. j in LSeg (f,j) by ;
then f /. j in (LSeg (f,j)) /\ (LSeg (f,(j + 1))) by ;
then f /. j = f /. (j + 1) by ;
hence contradiction by A19, A17, Th29; :: thesis: verum
end;
suppose (f /. j) `1 >= (f /. ((j + 1) + 1)) `1 ; :: thesis: contradiction
then f /. ((j + 1) + 1) in LSeg ((f /. j),(f /. (j + 1))) by A20, A18, A22, A24, Th8;
then A27: f /. ((j + 1) + 1) in LSeg (f,j) by ;
(j + 1) + 1 = j + (1 + 1) ;
then A28: (LSeg (f,j)) /\ (LSeg (f,(j + 1))) = {(f /. (j + 1))} by ;
f /. ((j + 1) + 1) in LSeg (f,(j + 1)) by ;
then f /. ((j + 1) + 1) in (LSeg (f,j)) /\ (LSeg (f,(j + 1))) by ;
then f /. ((j + 1) + 1) = f /. (j + 1) by ;
hence contradiction by A17, A21, Th29; :: thesis: verum
end;
end;
end;
hence contradiction ; :: thesis: verum
end;
suppose A29: (f /. ((j + 1) + 1)) `1 = (f /. (j + 1)) `1 ; :: thesis: contradiction
(f /. ((j + 1) + 1)) `2 = (f /. 1) `2 by
.= (f /. (j + 1)) `2 by ;
then f /. ((j + 1) + 1) = |[((f /. (j + 1)) `1),((f /. (j + 1)) `2)]| by
.= f /. (j + 1) by EUCLID:53 ;
hence contradiction by A17, A21, Th29; :: thesis: verum
end;
end;
end;
A30: ((len f) -' 1) + 1 = len f by ;
then A31: ( 2 <= (len f) -' 1 & (len f) -' 1 < len f ) by ;
A32: S1[ 0 ] ;
A33: for j being Nat holds S1[j] from NAT_1:sch 2(A32, A9);
then A34: (f /. ((len f) -' 1)) `1 <= (f /. 2) `1 by A31;
(f /. (len f)) `1 < (f /. ((len f) -' 1)) `1 by ;
then (f /. (len f)) `1 < (f /. 2) `1 by ;
hence contradiction by A8, FINSEQ_6:def 1; :: thesis: verum
end;
suppose A35: (f /. 2) `1 > (f /. 1) `1 ; :: thesis: contradiction
defpred S1[ Nat] means ( 2 <= \$1 & \$1 < len f implies ( (f /. \$1) `1 >= (f /. 2) `1 & (f /. (\$1 + 1)) `1 > (f /. \$1) `1 ) );
A36: for j being Nat st S1[j] holds
S1[j + 1]
proof
let j be Nat; :: thesis: ( S1[j] implies S1[j + 1] )
assume that
A37: ( 2 <= j & j < len f implies ( (f /. j) `1 >= (f /. 2) `1 & (f /. (j + 1)) `1 > (f /. j) `1 ) ) and
A38: 2 <= j + 1 and
A39: j + 1 < len f ; :: thesis: ( (f /. (j + 1)) `1 >= (f /. 2) `1 & (f /. ((j + 1) + 1)) `1 > (f /. (j + 1)) `1 )
1 + 1 <= j + 1 by A38;
then A40: 1 <= j by XREAL_1:6;
thus (f /. (j + 1)) `1 >= (f /. 2) `1 :: thesis: (f /. ((j + 1) + 1)) `1 > (f /. (j + 1)) `1
proof
per cases ( 2 = j + 1 or 2 < j + 1 ) by ;
suppose 2 = j + 1 ; :: thesis: (f /. (j + 1)) `1 >= (f /. 2) `1
hence (f /. (j + 1)) `1 >= (f /. 2) `1 ; :: thesis: verum
end;
suppose 2 < j + 1 ; :: thesis: (f /. (j + 1)) `1 >= (f /. 2) `1
hence (f /. (j + 1)) `1 >= (f /. 2) `1 by ; :: thesis: verum
end;
end;
end;
A41: (j + 1) + 1 <= len f by ;
A42: now :: thesis: (f /. (j + 1)) `1 > (f /. j) `1
per cases ( 1 + 1 = j + 1 or 2 < j + 1 ) by ;
suppose 1 + 1 = j + 1 ; :: thesis: (f /. (j + 1)) `1 > (f /. j) `1
hence (f /. (j + 1)) `1 > (f /. j) `1 by A35; :: thesis: verum
end;
suppose 2 < j + 1 ; :: thesis: (f /. (j + 1)) `1 > (f /. j) `1
hence (f /. (j + 1)) `1 > (f /. j) `1 by ; :: thesis: verum
end;
end;
end;
A43: 1 <= j + 1 by NAT_1:11;
then A44: j + 1 in dom f by ;
then A45: (f /. (j + 1)) `2 = (f /. 1) `2 by A1;
j < len f by ;
then A46: j in dom f by ;
then A47: (f /. j) `2 = (f /. 1) `2 by A1;
1 <= (j + 1) + 1 by NAT_1:11;
then A48: (j + 1) + 1 in dom f by ;
then A49: (f /. ((j + 1) + 1)) `2 = (f /. 1) `2 by A1;
assume A50: (f /. ((j + 1) + 1)) `1 <= (f /. (j + 1)) `1 ; :: thesis: contradiction
per cases ( (f /. ((j + 1) + 1)) `1 < (f /. (j + 1)) `1 or (f /. ((j + 1) + 1)) `1 = (f /. (j + 1)) `1 ) by ;
suppose A51: (f /. ((j + 1) + 1)) `1 < (f /. (j + 1)) `1 ; :: thesis: contradiction
per cases ) `1 >= (f /. ((j + 1) + 1)) `1 or (f /. j) `1 <= (f /. ((j + 1) + 1)) `1 ) ;
suppose (f /. j) `1 >= (f /. ((j + 1) + 1)) `1 ; :: thesis: contradiction
then f /. j in LSeg ((f /. (j + 1)),(f /. ((j + 1) + 1))) by A42, A47, A45, A49, Th8;
then A52: f /. j in LSeg (f,(j + 1)) by ;
(j + 1) + 1 = j + (1 + 1) ;
then A53: (LSeg (f,j)) /\ (LSeg (f,(j + 1))) = {(f /. (j + 1))} by ;
f /. j in LSeg (f,j) by ;
then f /. j in (LSeg (f,j)) /\ (LSeg (f,(j + 1))) by ;
then f /. j = f /. (j + 1) by ;
hence contradiction by A46, A44, Th29; :: thesis: verum
end;
suppose (f /. j) `1 <= (f /. ((j + 1) + 1)) `1 ; :: thesis: contradiction
then f /. ((j + 1) + 1) in LSeg ((f /. j),(f /. (j + 1))) by A47, A45, A49, A51, Th8;
then A54: f /. ((j + 1) + 1) in LSeg (f,j) by ;
(j + 1) + 1 = j + (1 + 1) ;
then A55: (LSeg (f,j)) /\ (LSeg (f,(j + 1))) = {(f /. (j + 1))} by ;
f /. ((j + 1) + 1) in LSeg (f,(j + 1)) by ;
then f /. ((j + 1) + 1) in (LSeg (f,j)) /\ (LSeg (f,(j + 1))) by ;
then f /. ((j + 1) + 1) = f /. (j + 1) by ;
hence contradiction by A44, A48, Th29; :: thesis: verum
end;
end;
end;
hence contradiction ; :: thesis: verum
end;
suppose A56: (f /. ((j + 1) + 1)) `1 = (f /. (j + 1)) `1 ; :: thesis: contradiction
(f /. ((j + 1) + 1)) `2 = (f /. 1) `2 by
.= (f /. (j + 1)) `2 by ;
then f /. ((j + 1) + 1) = |[((f /. (j + 1)) `1),((f /. (j + 1)) `2)]| by
.= f /. (j + 1) by EUCLID:53 ;
hence contradiction by A44, A48, Th29; :: thesis: verum
end;
end;
end;
A57: ((len f) -' 1) + 1 = len f by ;
then A58: ( 2 <= (len f) -' 1 & (len f) -' 1 < len f ) by ;
A59: S1[ 0 ] ;
A60: for j being Nat holds S1[j] from then A61: (f /. ((len f) -' 1)) `1 >= (f /. 2) `1 by A58;
(f /. (len f)) `1 > (f /. ((len f) -' 1)) `1 by ;
then (f /. (len f)) `1 > (f /. 2) `1 by ;
hence contradiction by A35, FINSEQ_6:def 1; :: thesis: verum
end;
end;