let f be constant standard special_circular_sequence; :: thesis: for i2 being Nat st 1 <= i2 & i2 + 1 < len f holds
f /^ i2 is being_S-Seq
let i2 be Nat; :: thesis: ( 1 <= i2 & i2 + 1 < len f implies f /^ i2 is being_S-Seq )
assume that
A1: 1 <= i2 and
A2: i2 + 1 < len f ; :: thesis: f /^ i2 is being_S-Seq
A3: i2 < len f by A2, NAT_1:13;
for i, j being Nat st i + 1 < j holds
LSeg ((f /^ i2),i) misses LSeg ((f /^ i2),j)

proof

let i, j be Nat; :: thesis: ( i + 1 < j implies LSeg ((f /^ i2),i) misses LSeg ((f /^ i2),j) )
assume A4: i + 1 < j ; :: thesis: LSeg ((f /^ i2),i) misses LSeg ((f /^ i2),j)
then A5: i < j by NAT_1:13;

now :: thesis: ( ( 1 <= i & j < len (f /^ i2) & LSeg ((f /^ i2),i) misses LSeg ((f /^ i2),j) ) or ( ( 1 > i or j >= len (f /^ i2) ) & LSeg ((f /^ i2),i) misses LSeg ((f /^ i2),j) ) )

per cases ( ( 1 <= i & j < len (f /^ i2) ) or 1 > i or j >= len (f /^ i2) ) ;

case A6: ( 1 <= i & j < len (f /^ i2) ) ; :: thesis: LSeg ((f /^ i2),i) misses LSeg ((f /^ i2),j)

then 1 < j by A5, XXREAL_0:2;
then LSeg ((f /^ i2),j) = LSeg (f,(i2 + j)) by A3, SPPOL_2:4;
then A7: (LSeg ((f /^ i2),i)) /\ (LSeg ((f /^ i2),j)) = (LSeg (f,(i2 + i))) /\ (LSeg (f,(i2 + j))) by A3, A6, SPPOL_2:4;
i2 + (i + 1) < i2 + j by A4, XREAL_1:6;
then A8: (i2 + i) + 1 < i2 + j ;
1 + 1 <= i2 + i by A1, A6, XREAL_1:7;
then A9: 1 < i2 + i by XXREAL_0:2;
j < (len f) - i2 by A3, A6, RFINSEQ:def 1;
then j + i2 < ((len f) - i2) + i2 by XREAL_1:6;
then LSeg (f,(i2 + i)) misses LSeg (f,(i2 + j)) by A8, A9, GOBOARD5:def 4;
then (LSeg (f,(i2 + i))) /\ (LSeg (f,(i2 + j))) = {} by XBOOLE_0:def 7;
hence LSeg ((f /^ i2),i) misses LSeg ((f /^ i2),j) by A7, XBOOLE_0:def 7; :: thesis: verum

end;

case A10: ( 1 > i or j >= len (f /^ i2) ) ; :: thesis: LSeg ((f /^ i2),i) misses LSeg ((f /^ i2),j)

now :: thesis: ( ( 1 > i & LSeg ((f /^ i2),i) misses LSeg ((f /^ i2),j) ) or ( j >= len (f /^ i2) & LSeg ((f /^ i2),i) misses LSeg ((f /^ i2),j) ) )

per cases ( 1 > i or j >= len (f /^ i2) ) by A10;

case 1 > i ; :: thesis: LSeg ((f /^ i2),i) misses LSeg ((f /^ i2),j)

then LSeg ((f /^ i2),i) = {} by TOPREAL1:def 3;
then (LSeg ((f /^ i2),i)) /\ (LSeg ((f /^ i2),j)) = {} ;
hence LSeg ((f /^ i2),i) misses LSeg ((f /^ i2),j) by XBOOLE_0:def 7; :: thesis: verum

end;

case j >= len (f /^ i2) ; :: thesis: LSeg ((f /^ i2),i) misses LSeg ((f /^ i2),j)

then j + 1 > len (f /^ i2) by NAT_1:13;
then LSeg ((f /^ i2),j) = {} by TOPREAL1:def 3;
then (LSeg ((f /^ i2),i)) /\ (LSeg ((f /^ i2),j)) = {} ;
hence LSeg ((f /^ i2),i) misses LSeg ((f /^ i2),j) by XBOOLE_0:def 7; :: thesis: verum

end;

end;

end;

hence LSeg ((f /^ i2),i) misses LSeg ((f /^ i2),j) ; :: thesis: verum

end;

end;

end;

hence LSeg ((f /^ i2),i) misses LSeg ((f /^ i2),j) ; :: thesis: verum

end;

then A11: f /^ i2 is s.n.c. by TOPREAL1:def 7;
A12: len (f /^ i2) = (len f) - i2 by A3, RFINSEQ:def 1;
for n1, n2 being Nat st 1 <= n1 & n1 <= len (f /^ i2) & 1 <= n2 & n2 <= len (f /^ i2) & ( (f /^ i2) . n1 = (f /^ i2) . n2 or (f /^ i2) /. n1 = (f /^ i2) /. n2 ) holds
n1 = n2

proof

let n1, n2 be Nat; :: thesis: ( 1 <= n1 & n1 <= len (f /^ i2) & 1 <= n2 & n2 <= len (f /^ i2) & ( (f /^ i2) . n1 = (f /^ i2) . n2 or (f /^ i2) /. n1 = (f /^ i2) /. n2 ) implies n1 = n2 )
assume that
A13: 1 <= n1 and
A14: n1 <= len (f /^ i2) and
A15: 1 <= n2 and
A16: n2 <= len (f /^ i2) and
A17: ( (f /^ i2) . n1 = (f /^ i2) . n2 or (f /^ i2) /. n1 = (f /^ i2) /. n2 ) ; :: thesis: n1 = n2
A18: n2 in dom (f /^ i2) by A15, A16, FINSEQ_3:25;
A19: n1 in dom (f /^ i2) by A13, A14, FINSEQ_3:25;

now :: thesis: ( ( n1 < n2 & contradiction ) or ( n1 = n2 & n1 = n2 ) or ( n2 < n1 & contradiction ) )

per cases ( n1 < n2 or n1 = n2 or n2 < n1 ) by XXREAL_0:1;

case n1 < n2 ; :: thesis: contradiction

then A20: i2 + n1 < i2 + n2 by XREAL_1:6;
A21: 1 < i2 + 1 by A1, NAT_1:13;
i2 + 1 <= i2 + n1 by A13, XREAL_1:6;
then A22: 1 < i2 + n1 by A21, XXREAL_0:2;
n2 + i2 <= ((len f) - i2) + i2 by A12, A16, XREAL_1:6;
then A23: f /. (i2 + n1) <> f /. (i2 + n2) by A22, A20, GOBOARD7:37;
A24: (f /^ i2) /. n1 = f /. (i2 + n1) by A19, FINSEQ_5:27;
A25: (f /^ i2) /. n2 = f /. (i2 + n2) by A18, FINSEQ_5:27;
(f /^ i2) /. n1 = (f /^ i2) . n1 by A13, A14, FINSEQ_4:15;
hence contradiction by A15, A16, A17, A23, A24, A25, FINSEQ_4:15; :: thesis: verum

end;

case n1 = n2 ; :: thesis: n1 = n2

hence n1 = n2 ; :: thesis: verum

end;

case n2 < n1 ; :: thesis: contradiction

then A26: i2 + n2 < i2 + n1 by XREAL_1:6;
A27: 1 < i2 + 1 by A1, NAT_1:13;
i2 + 1 <= i2 + n2 by A15, XREAL_1:6;
then A28: 1 < i2 + n2 by A27, XXREAL_0:2;
n1 + i2 <= ((len f) - i2) + i2 by A12, A14, XREAL_1:6;
then A29: f /. (i2 + n2) <> f /. (i2 + n1) by A28, A26, GOBOARD7:37;
n2 in dom (f /^ i2) by A15, A16, FINSEQ_3:25;
then A30: (f /^ i2) /. n2 = f /. (i2 + n2) by FINSEQ_5:27;
n1 in dom (f /^ i2) by A13, A14, FINSEQ_3:25;
then A31: (f /^ i2) /. n1 = f /. (i2 + n1) by FINSEQ_5:27;
(f /^ i2) /. n2 = (f /^ i2) . n2 by A15, A16, FINSEQ_4:15;
hence contradiction by A13, A14, A17, A29, A30, A31, FINSEQ_4:15; :: thesis: verum

end;

end;

end;

hence n1 = n2 ; :: thesis: verum

end;

then A32: f /^ i2 is one-to-one by Th36;
(i2 + 1) - i2 < (len f) - i2 by A2, XREAL_1:9;
then 1 + 1 <= len (f /^ i2) by A12, NAT_1:13;
hence f /^ i2 is being_S-Seq by A11, A32, TOPREAL1:def 8; :: thesis: verum