let i, j be Nat; :: thesis: for f being V22() standard special_circular_sequence st 1 <= i & i < j & j <= len f & f /. 1 in L~ (mid (f,i,j)) & not i = 1 holds
j = len f
let f be V22() standard special_circular_sequence; :: thesis: ( 1 <= i & i < j & j <= len f & f /. 1 in L~ (mid (f,i,j)) & not i = 1 implies j = len f )
assume that
A1: 1 <= i and
A2: i < j and
A3: j <= len f ; :: thesis: ( not f /. 1 in L~ (mid (f,i,j)) or i = 1 or j = len f )
1 + 1 <= len f by GOBOARD7:34, XXREAL_0:2;
then A4: f /. 1 in LSeg (f,1) by TOPREAL1:21;
assume f /. 1 in L~ (mid (f,i,j)) ; :: thesis: ( i = 1 or j = len f )
then consider n being Nat such that
A5: 1 <= n and
A6: n + 1 <= len (mid (f,i,j)) and
A7: f /. 1 in LSeg ((mid (f,i,j)),n) by SPPOL_2:13;
n < len (mid (f,i,j)) by A6, NAT_1:13;
then A8: n < (j -' i) + 1 by A1, A2, A3, JORDAN4:8;
then LSeg ((mid (f,i,j)),n) = LSeg (f,((n + i) -' 1)) by A1, A2, A3, A5, JORDAN4:19;
then A9: f /. 1 in (LSeg (f,1)) /\ (LSeg (f,((n + i) -' 1))) by A7, A4, XBOOLE_0:def 4;
then A10: LSeg (f,1) meets LSeg (f,((n + i) -' 1)) ;
assume that
A11: i <> 1 and
A12: j <> len f ; :: thesis: contradiction
per cases ( 1 + 1 >= (n + i) -' 1 or ((n + i) -' 1) + 1 >= len f ) by A10, GOBOARD5:def 4;
suppose 1 + 1 >= (n + i) -' 1 ; :: thesis: contradiction
then A13: n + i <= 2 + 1 by NAT_D:52;
i > 1 by A1, A11, XXREAL_0:1;
then A14: i >= 1 + 1 by NAT_1:13;
n + i >= i + 1 by A5, XREAL_1:6;
then i + 1 <= 2 + 1 by A13, XXREAL_0:2;
then i <= 2 by XREAL_1:6;
then A15: i = 2 by A14, XXREAL_0:1;
then n <= 1 by A13, XREAL_1:6;
then n = 1 by A5, XXREAL_0:1;
then A16: (n + i) -' 1 = 2 by A15, NAT_D:34;
A17: 2 < len f by GOBOARD7:34, XXREAL_0:2;
1 + 2 <= len f by GOBOARD7:34, XXREAL_0:2;
then (LSeg (f,1)) /\ (LSeg (f,(1 + 1))) = {(f /. (1 + 1))} by TOPREAL1:def 6;
then f /. 1 = f /. 2 by A9, A16, TARSKI:def 1;
hence contradiction by A17, GOBOARD7:36; :: thesis: verum
end;
suppose A18: ((n + i) -' 1) + 1 >= len f ; :: thesis: contradiction
n <= n + i by NAT_1:11;
then A19: len f <= n + i by A5, A18, XREAL_1:235, XXREAL_0:2;
((j -' i) + 1) + i = ((j -' i) + i) + 1
.= j + 1 by A2, XREAL_1:235 ;
then n + i < j + 1 by A8, XREAL_1:6;
then A20: n + i <= j by NAT_1:13;
j < len f by A3, A12, XXREAL_0:1;
hence contradiction by A19, A20, XXREAL_0:2; :: thesis: verum
end;
end;