let f be V26() 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
i2 <= len f by A2, NAT_1:13;
then A3: len (f | i2) = i2 by FINSEQ_1:59;
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
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 :: 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 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 Th36;
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)
now :: thesis: ( ( 1 <= i & j + 1 <= len (f | i2) & LSeg ((f | i2),i) misses LSeg ((f | i2),j) ) or ( ( 1 > i or j + 1 > len (f | i2) ) & LSeg ((f | i2),i) misses LSeg ((f | i2),j) ) )
per cases ( ( 1 <= i & j + 1 <= len (f | i2) ) or 1 > i or j + 1 > len (f | i2) ) ;
case A23: ( 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 A23, NAT_1:13;
then j + 1 < len f by A2, XXREAL_0:2;
then A24: LSeg (f,i) misses LSeg (f,j) by A22, GOBOARD5:def 4;
A25: j <= len (f | i2) by A23, NAT_1:13;
LSeg ((f | i2),j) = LSeg (f,j) by A23, SPPOL_2:3;
then (LSeg ((f | i2),i)) /\ (LSeg ((f | i2),j)) = (LSeg (f,i)) /\ (LSeg (f,j)) by A22, A25, SPPOL_2:3, XXREAL_0:2;
then (LSeg ((f | i2),i)) /\ (LSeg ((f | i2),j)) = {} by A24, XBOOLE_0:def 7;
hence LSeg ((f | i2),i) misses LSeg ((f | i2),j) by XBOOLE_0:def 7; :: thesis: verum
end;
case A26: ( 1 > i or j + 1 > 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 + 1 > len (f | i2) & LSeg ((f | i2),i) misses LSeg ((f | i2),j) ) )
per cases ( 1 > i or j + 1 > len (f | i2) ) by A26;
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 A27: 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 A27, A21, TOPREAL1:def 8; :: thesis: verum