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 that
A1: 1 < i2 and
A2: i2 + 1 <= len f ; :: thesis: f | i2 is being_S-Seq
i2 <= len f by A2, NAT_1:13;
then A3: len (f | i2) = i2 by FINSEQ_1:59;
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 that
A4: 1 <= n1 and
A5: n1 <= len (f | i2) and
A6: 1 <= n2 and
A7: n2 <= len (f | i2) and
A8: ( (f | i2) . n1 = (f | i2) . n2 or (f | i2) /. n1 = (f | i2) /. n2 ) ; :: thesis: n1 = n2
A9: n2 in dom (f | i2) by A6, A7, FINSEQ_3:25;
A10: n1 in dom (f | i2) by A4, A5, FINSEQ_3:25;

now

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

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

n2 + 1 <= i2 + 1 by A3, A7, XREAL_1:6;
then n2 + 1 <= len f by A2, XXREAL_0:2;
then A12: n2 < len f by NAT_1:13;
len f > 4 by GOBOARD7:34;
then A13: f /. n1 <> f /. n2 by A4, A11, A12, GOBOARD7:35;
A14: (f | i2) /. n1 = f /. n1 by A10, FINSEQ_4:70;
A15: (f | i2) /. n2 = f /. n2 by A9, FINSEQ_4:70;
(f | i2) /. n1 = (f | i2) . n1 by A4, A5, FINSEQ_4:15;
hence contradiction by A6, A7, A8, A13, A14, A15, FINSEQ_4:15; :: thesis: verum

end;

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

hence n1 = n2 ; :: thesis: verum

end;

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

n1 + 1 <= i2 + 1 by A3, A5, XREAL_1:6;
then n1 + 1 <= len f by A2, XXREAL_0:2;
then A17: n1 < len f by NAT_1:13;
len f > 4 by GOBOARD7:34;
then A18: f /. n2 <> f /. n1 by A6, A16, A17, GOBOARD7:35;
A19: (f | i2) /. n2 = f /. n2 by A9, FINSEQ_4:70;
A20: (f | i2) /. n1 = f /. n1 by A10, FINSEQ_4:70;
(f | i2) /. n2 = (f | i2) . n2 by A6, A7, FINSEQ_4:15;
hence contradiction by A4, A5, A8, A18, A19, A20, FINSEQ_4:15; :: thesis: verum

end;

end;

end;

hence n1 = n2 ; :: thesis: verum

end;

then A21: f | i2 is one-to-one by Th48;
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 A22: i + 1 < j ; :: thesis: LSeg ((f | i2),i) misses LSeg ((f | i2),j)
A23: j in NAT by ORDINAL1:def 12;
A24: i in NAT by ORDINAL1:def 12;

now

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

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

i2 <= len f by A2, NAT_1:13;
then len (f | i2) = i2 by FINSEQ_1:59;
then j + 1 < i2 + 1 by A25, NAT_1:13;
then j + 1 < len f by A2, XXREAL_0:2;
then A26: LSeg (f,i) misses LSeg (f,j) by A22, A24, A23, GOBOARD5:def 4;
A27: j <= len (f | i2) by A25, NAT_1:13;
LSeg ((f | i2),j) = LSeg (f,j) by A25, SPPOL_2:3;
then (LSeg ((f | i2),i)) /\ (LSeg ((f | i2),j)) = (LSeg (f,i)) /\ (LSeg (f,j)) by A22, A27, SPPOL_2:3, XXREAL_0:2;
then (LSeg ((f | i2),i)) /\ (LSeg ((f | i2),j)) = {} by A26, XBOOLE_0:def 7;
hence LSeg ((f | i2),i) misses LSeg ((f | i2),j) by XBOOLE_0:def 7; :: thesis: verum

end;

case A28: ( 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 A28;

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

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 A29: f | i2 is s.n.c. by TOPREAL1:def 7;
1 + 1 <= len (f | i2) by A1, A3, NAT_1:13;
hence f | i2 is being_S-Seq by A29, A21, TOPREAL1:def 8; :: thesis: verum