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 i2 <= len f by NAT_1:13;
then A2: len (f | i2) = i2 by FINSEQ_1:80;
then A3: 1 + 1 <= len (f | i2) by A1, 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
A5: ( i in NAT & j in NAT ) by ORDINAL1:def 13;

now

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

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

then A7: LSeg (f | i2),j = LSeg f,j by SPPOL_2:3;
j <= len (f | i2) by A6, NAT_1:13;
then A8: (LSeg (f | i2),i) /\ (LSeg (f | i2),j) = (LSeg f,i) /\ (LSeg f,j) by A4, A7, SPPOL_2:3, XXREAL_0:2;
i2 <= len f by A1, NAT_1:13;
then len (f | i2) = i2 by FINSEQ_1:80;
then j + 1 < i2 + 1 by A6, NAT_1:13;
then j + 1 < len f by A1, XXREAL_0:2;
then LSeg f,i misses LSeg f,j by A4, A5, GOBOARD5:def 4;
then (LSeg (f | i2),i) /\ (LSeg (f | i2),j) = {} by A8, XBOOLE_0:def 7;
hence LSeg (f | i2),i misses LSeg (f | i2),j by XBOOLE_0:def 7; :: thesis: verum

end;

case A9: ( 1 > i or j + 1 > len (f | i2) ) ; :: thesis: LSeg (f | i2),i misses LSeg (f | i2),j

now

per cases ( 1 > i or j + 1 > len (f | i2) ) by A9;

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 + 1 > len (f | i2) ; :: thesis: LSeg (f | i2),i misses LSeg (f | i2),j

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 A10: 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 A11: ( 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 A12: n1 in dom (f | i2) by FINSEQ_3:27;
A13: n2 in dom (f | i2) by A11, FINSEQ_3:27;

now

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

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

n2 + 1 <= i2 + 1 by A2, A11, XREAL_1:8;
then n2 + 1 <= len f by A1, XXREAL_0:2;
then A15: n2 < len f by NAT_1:13;
len f > 4 by GOBOARD7:36;
then A16: f /. n1 <> f /. n2 by A11, A14, A15, GOBOARD7:37;
A17: (f | i2) /. n1 = f /. n1 by A12, FINSEQ_4:85;
A18: (f | i2) /. n2 = f /. n2 by A13, FINSEQ_4:85;
(f | i2) /. n1 = (f | i2) . n1 by A11, FINSEQ_4:24;
hence contradiction by A11, A16, A17, A18, FINSEQ_4:24; :: thesis: verum

end;

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

hence n1 = n2 ; :: thesis: verum

end;

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

n1 + 1 <= i2 + 1 by A2, A11, XREAL_1:8;
then n1 + 1 <= len f by A1, XXREAL_0:2;
then A20: n1 < len f by NAT_1:13;
len f > 4 by GOBOARD7:36;
then A21: f /. n2 <> f /. n1 by A11, A19, A20, GOBOARD7:37;
A22: (f | i2) /. n2 = f /. n2 by A13, FINSEQ_4:85;
A23: (f | i2) /. n1 = f /. n1 by A12, FINSEQ_4:85;
(f | i2) /. n2 = (f | i2) . n2 by A11, FINSEQ_4:24;
hence contradiction by A11, A21, A22, A23, 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 A3, A10, TOPREAL1:def 10; :: thesis: verum