let f be non constant standard special_circular_sequence; :: thesis: for i2 being Element of NAT st 1 <= i2 & i2 + 1 < len f holds
f /^ i2 is being_S-Seq
let i2 be Element of NAT ; :: thesis: ( 1 <= i2 & i2 + 1 < len f implies f /^ i2 is being_S-Seq )
assume A1: ( 1 <= i2 & i2 + 1 < len f ) ; :: thesis: f /^ i2 is being_S-Seq
then A2: i2 < len f by NAT_1:13;
then A3: len (f /^ i2) = (len f) - i2 by RFINSEQ:def 2;
(i2 + 1) - i2 < (len f) - i2 by A1, XREAL_1:11;
then A4: 1 + 1 <= len (f /^ i2) by A3, 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 A5: i + 1 < j ; :: thesis: LSeg (f /^ i2),i misses LSeg (f /^ i2),j
then A6: i < j by NAT_1:13;

now

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

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

then 1 < j by A6, XXREAL_0:2;
then A8: LSeg (f /^ i2),j = LSeg f,(i2 + j) by A2, SPPOL_2:4;
A9: j < (len f) - i2 by A2, A7, RFINSEQ:def 2;
A10: (LSeg (f /^ i2),i) /\ (LSeg (f /^ i2),j) = (LSeg f,(i2 + i)) /\ (LSeg f,(i2 + j)) by A2, A7, A8, SPPOL_2:4;
i2 + (i + 1) < i2 + j by A5, XREAL_1:8;
then A11: (i2 + i) + 1 < i2 + j ;
A12: 1 + 1 <= i2 + i by A1, A7, XREAL_1:9;
j + i2 < ((len f) - i2) + i2 by A9, XREAL_1:8;
then ( 1 < i2 + i & i2 + j < len f ) by A12, XXREAL_0:2;
then LSeg f,(i2 + i) misses LSeg f,(i2 + j) by A11, 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 A10, XBOOLE_0:def 7; :: thesis: verum

end;

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

now

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

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

then LSeg (f /^ i2),i = {} by TOPREAL1:def 5;
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 5;
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 A14: f /^ i2 is s.n.c. by TOPREAL1:def 9;
f /^ i2 is one-to-one

proof

for n1, n2 being Element of 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 Element of 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 A15: ( 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 ) ) ; :: thesis: n1 = n2
then A16: n1 in dom (f /^ i2) by FINSEQ_3:27;
A17: n2 in dom (f /^ i2) by A15, FINSEQ_3:27;

now

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

case A18: n1 < n2 ; :: thesis: contradiction

A19: n2 + i2 <= ((len f) - i2) + i2 by A3, A15, XREAL_1:8;
A20: i2 + 1 <= i2 + n1 by A15, XREAL_1:8;
1 < i2 + 1 by A1, NAT_1:13;
then A21: 1 < i2 + n1 by A20, XXREAL_0:2;
i2 + n1 < i2 + n2 by A18, XREAL_1:8;
then A22: f /. (i2 + n1) <> f /. (i2 + n2) by A19, A21, GOBOARD7:39;
A23: (f /^ i2) /. n1 = f /. (i2 + n1) by A16, FINSEQ_5:30;
A24: (f /^ i2) /. n2 = f /. (i2 + n2) by A17, FINSEQ_5:30;
(f /^ i2) /. n1 = (f /^ i2) . n1 by A15, FINSEQ_4:24;
hence contradiction by A15, A22, A23, A24, FINSEQ_4:24; :: thesis: verum

end;

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

hence n1 = n2 ; :: thesis: verum

end;

case A25: n2 < n1 ; :: thesis: contradiction

A26: n1 + i2 <= ((len f) - i2) + i2 by A3, A15, XREAL_1:8;
A27: i2 + 1 <= i2 + n2 by A15, XREAL_1:8;
1 < i2 + 1 by A1, NAT_1:13;
then A28: 1 < i2 + n2 by A27, XXREAL_0:2;
i2 + n2 < i2 + n1 by A25, XREAL_1:8;
then A29: f /. (i2 + n2) <> f /. (i2 + n1) by A26, A28, GOBOARD7:39;
n2 in dom (f /^ i2) by A15, FINSEQ_3:27;
then A30: (f /^ i2) /. n2 = f /. (i2 + n2) by FINSEQ_5:30;
n1 in dom (f /^ i2) by A15, FINSEQ_3:27;
then A31: (f /^ i2) /. n1 = f /. (i2 + n1) by FINSEQ_5:30;
(f /^ i2) /. n2 = (f /^ i2) . n2 by A15, FINSEQ_4:24;
hence contradiction by A15, A29, A30, A31, FINSEQ_4:24; :: thesis: verum

end;

end;

end;

hence n1 = n2 ; :: thesis: verum

end;

hence f /^ i2 is one-to-one by Th48; :: thesis: verum

end;

hence f /^ i2 is being_S-Seq by A4, A14, TOPREAL1:def 10; :: thesis: verum