reconsider ff = Rev f as non empty FinSequence of (TOP-REAL 2) ;

A1: Rev ff = f ;

A2: GoB ff = GoB f by Lm1;

A3: f is_sequence_on GoB f by GOBOARD5:def 5;

A4: len f = len ff by FINSEQ_5:def 3;

A5: ff is standard

.= f /. 1 by FINSEQ_6:def 1

.= ff /. (len ff) by A4, FINSEQ_5:65 ;

ff is s.c.c.

A1: Rev ff = f ;

A2: GoB ff = GoB f by Lm1;

A3: f is_sequence_on GoB f by GOBOARD5:def 5;

A4: len f = len ff by FINSEQ_5:def 3;

A5: ff is standard

proof
_{1}, b_{2}, b_{3}, b_{4} being set holds

( not [b_{1},b_{2}] in Indices (GoB ff) or not [b_{3},b_{4}] in Indices (GoB ff) or not ff /. k = (GoB ff) * (b_{1},b_{2}) or not ff /. (k + 1) = (GoB ff) * (b_{3},b_{4}) or |.(b_{1} - b_{3}).| + |.(b_{2} - b_{4}).| = 1 ) )

assume that

A11: k in dom ff and

A12: k + 1 in dom ff ; :: thesis: for b_{1}, b_{2}, b_{3}, b_{4} being set holds

( not [b_{1},b_{2}] in Indices (GoB ff) or not [b_{3},b_{4}] in Indices (GoB ff) or not ff /. k = (GoB ff) * (b_{1},b_{2}) or not ff /. (k + 1) = (GoB ff) * (b_{3},b_{4}) or |.(b_{1} - b_{3}).| + |.(b_{2} - b_{4}).| = 1 )

set l = ((len f) + 1) -' (k + 1);

k <= len f by A4, A11, FINSEQ_3:25;

then k + 1 <= (len f) + 1 by XREAL_1:6;

then A13: (((len f) + 1) -' (k + 1)) + (k + 1) = (len f) + 1 by XREAL_1:235;

then A14: ((len f) + 1) -' (k + 1) in dom f by A1, A4, A12, FINSEQ_5:59;

A15: ((((len f) + 1) -' (k + 1)) + 1) + k = (len f) + 1 by A13;

then A16: (((len f) + 1) -' (k + 1)) + 1 in dom f by A1, A4, A11, FINSEQ_5:59;

let i1, j1, i2, j2 be Nat; :: thesis: ( not [i1,j1] in Indices (GoB ff) or not [i2,j2] in Indices (GoB ff) or not ff /. k = (GoB ff) * (i1,j1) or not ff /. (k + 1) = (GoB ff) * (i2,j2) or |.(i1 - i2).| + |.(j1 - j2).| = 1 )

assume that

A17: [i1,j1] in Indices (GoB ff) and

A18: [i2,j2] in Indices (GoB ff) and

A19: ff /. k = (GoB ff) * (i1,j1) and

A20: ff /. (k + 1) = (GoB ff) * (i2,j2) ; :: thesis: |.(i1 - i2).| + |.(j1 - j2).| = 1

A21: |.(i2 - i1).| = |.(- (i1 - i2)).|

.= |.(i1 - i2).| by COMPLEX1:52 ;

A22: |.(j2 - j1).| = |.(- (j1 - j2)).|

.= |.(j1 - j2).| by COMPLEX1:52 ;

A23: f /. (((len f) + 1) -' (k + 1)) = (GoB f) * (i2,j2) by A1, A2, A4, A12, A13, A20, FINSEQ_5:66;

f /. ((((len f) + 1) -' (k + 1)) + 1) = (GoB f) * (i1,j1) by A1, A2, A4, A11, A15, A19, FINSEQ_5:66;

hence |.(i1 - i2).| + |.(j1 - j2).| = 1 by A2, A3, A14, A16, A17, A18, A21, A22, A23; :: thesis: verum

end;

A24: ff /. 1 =
f /. (len f)
by FINSEQ_5:65
hereby :: according to GOBOARD5:def 5,GOBOARD1:def 9 :: thesis: for b_{1} being set holds

( not b_{1} in dom ff or not b_{1} + 1 in dom ff or for b_{2}, b_{3}, b_{4}, b_{5} being set holds

( not [b_{2},b_{3}] in Indices (GoB ff) or not [b_{4},b_{5}] in Indices (GoB ff) or not ff /. b_{1} = (GoB ff) * (b_{2},b_{3}) or not ff /. (b_{1} + 1) = (GoB ff) * (b_{4},b_{5}) or |.(b_{2} - b_{4}).| + |.(b_{3} - b_{5}).| = 1 ) )

let k be Nat; :: thesis: ( not k in dom ff or not k + 1 in dom ff or for b( not b

( not [b

let k be Nat; :: thesis: ( k in dom ff implies ex i, j being Nat st

( [i,j] in Indices (GoB ff) & ff /. k = (GoB ff) * (i,j) ) )

assume A6: k in dom ff ; :: thesis: ex i, j being Nat st

( [i,j] in Indices (GoB ff) & ff /. k = (GoB ff) * (i,j) )

set l = ((len f) + 1) -' k;

A7: k <= len f by A4, A6, FINSEQ_3:25;

len f < (len f) + 1 by NAT_1:13;

then A8: (((len f) + 1) -' k) + k = (len f) + 1 by A7, XREAL_1:235, XXREAL_0:2;

then ((len f) + 1) -' k in dom f by A1, A4, A6, FINSEQ_5:59;

then consider i, j being Nat such that

A9: [i,j] in Indices (GoB f) and

A10: f /. (((len f) + 1) -' k) = (GoB f) * (i,j) by A3;

take i = i; :: thesis: ex j being Nat st

( [i,j] in Indices (GoB ff) & ff /. k = (GoB ff) * (i,j) )

take j = j; :: thesis: ( [i,j] in Indices (GoB ff) & ff /. k = (GoB ff) * (i,j) )

thus [i,j] in Indices (GoB ff) by A9, Lm1; :: thesis: ff /. k = (GoB ff) * (i,j)

thus ff /. k = (GoB ff) * (i,j) by A1, A2, A4, A6, A8, A10, FINSEQ_5:66; :: thesis: verum

end;( [i,j] in Indices (GoB ff) & ff /. k = (GoB ff) * (i,j) ) )

assume A6: k in dom ff ; :: thesis: ex i, j being Nat st

( [i,j] in Indices (GoB ff) & ff /. k = (GoB ff) * (i,j) )

set l = ((len f) + 1) -' k;

A7: k <= len f by A4, A6, FINSEQ_3:25;

len f < (len f) + 1 by NAT_1:13;

then A8: (((len f) + 1) -' k) + k = (len f) + 1 by A7, XREAL_1:235, XXREAL_0:2;

then ((len f) + 1) -' k in dom f by A1, A4, A6, FINSEQ_5:59;

then consider i, j being Nat such that

A9: [i,j] in Indices (GoB f) and

A10: f /. (((len f) + 1) -' k) = (GoB f) * (i,j) by A3;

take i = i; :: thesis: ex j being Nat st

( [i,j] in Indices (GoB ff) & ff /. k = (GoB ff) * (i,j) )

take j = j; :: thesis: ( [i,j] in Indices (GoB ff) & ff /. k = (GoB ff) * (i,j) )

thus [i,j] in Indices (GoB ff) by A9, Lm1; :: thesis: ff /. k = (GoB ff) * (i,j)

thus ff /. k = (GoB ff) * (i,j) by A1, A2, A4, A6, A8, A10, FINSEQ_5:66; :: thesis: verum

( not [b

assume that

A11: k in dom ff and

A12: k + 1 in dom ff ; :: thesis: for b

( not [b

set l = ((len f) + 1) -' (k + 1);

k <= len f by A4, A11, FINSEQ_3:25;

then k + 1 <= (len f) + 1 by XREAL_1:6;

then A13: (((len f) + 1) -' (k + 1)) + (k + 1) = (len f) + 1 by XREAL_1:235;

then A14: ((len f) + 1) -' (k + 1) in dom f by A1, A4, A12, FINSEQ_5:59;

A15: ((((len f) + 1) -' (k + 1)) + 1) + k = (len f) + 1 by A13;

then A16: (((len f) + 1) -' (k + 1)) + 1 in dom f by A1, A4, A11, FINSEQ_5:59;

let i1, j1, i2, j2 be Nat; :: thesis: ( not [i1,j1] in Indices (GoB ff) or not [i2,j2] in Indices (GoB ff) or not ff /. k = (GoB ff) * (i1,j1) or not ff /. (k + 1) = (GoB ff) * (i2,j2) or |.(i1 - i2).| + |.(j1 - j2).| = 1 )

assume that

A17: [i1,j1] in Indices (GoB ff) and

A18: [i2,j2] in Indices (GoB ff) and

A19: ff /. k = (GoB ff) * (i1,j1) and

A20: ff /. (k + 1) = (GoB ff) * (i2,j2) ; :: thesis: |.(i1 - i2).| + |.(j1 - j2).| = 1

A21: |.(i2 - i1).| = |.(- (i1 - i2)).|

.= |.(i1 - i2).| by COMPLEX1:52 ;

A22: |.(j2 - j1).| = |.(- (j1 - j2)).|

.= |.(j1 - j2).| by COMPLEX1:52 ;

A23: f /. (((len f) + 1) -' (k + 1)) = (GoB f) * (i2,j2) by A1, A2, A4, A12, A13, A20, FINSEQ_5:66;

f /. ((((len f) + 1) -' (k + 1)) + 1) = (GoB f) * (i1,j1) by A1, A2, A4, A11, A15, A19, FINSEQ_5:66;

hence |.(i1 - i2).| + |.(j1 - j2).| = 1 by A2, A3, A14, A16, A17, A18, A21, A22, A23; :: thesis: verum

.= f /. 1 by FINSEQ_6:def 1

.= ff /. (len ff) by A4, FINSEQ_5:65 ;

ff is s.c.c.

proof

hence
Rev f is standard special_circular_sequence
by A5, A24, FINSEQ_6:def 1, SPPOL_2:28, SPPOL_2:40; :: thesis: verum
let i be Nat; :: according to GOBOARD5:def 4 :: thesis: for b_{1} being set holds

( b_{1} <= i + 1 or ( ( i <= 1 or len ff <= b_{1} ) & len ff <= b_{1} + 1 ) or LSeg (ff,i) misses LSeg (ff,b_{1}) )

let j be Nat; :: thesis: ( j <= i + 1 or ( ( i <= 1 or len ff <= j ) & len ff <= j + 1 ) or LSeg (ff,i) misses LSeg (ff,j) )

assume that

A25: i + 1 < j and

A26: ( ( i > 1 & j < len ff ) or j + 1 < len ff ) ; :: thesis: LSeg (ff,i) misses LSeg (ff,j)

set k = (len f) -' i;

set l = (len f) -' j;

A27: j <= len f by A4, A26, NAT_1:13;

then A28: ((len f) -' j) + j = len f by XREAL_1:235;

i < j by A25, NAT_1:13;

then A29: ((len f) -' i) + i = len f by A27, XREAL_1:235, XXREAL_0:2;

then (i + 1) + ((len f) -' i) = (((len f) -' j) + 1) + j by A28;

then (((len f) -' j) + 1) + j < j + ((len f) -' i) by A25, XREAL_1:6;

then A30: ((len f) -' j) + 1 < (len f) -' i by XREAL_1:6;

A31: j + 1 <= len f by A4, A26, NAT_1:13;

end;( b

let j be Nat; :: thesis: ( j <= i + 1 or ( ( i <= 1 or len ff <= j ) & len ff <= j + 1 ) or LSeg (ff,i) misses LSeg (ff,j) )

assume that

A25: i + 1 < j and

A26: ( ( i > 1 & j < len ff ) or j + 1 < len ff ) ; :: thesis: LSeg (ff,i) misses LSeg (ff,j)

set k = (len f) -' i;

set l = (len f) -' j;

A27: j <= len f by A4, A26, NAT_1:13;

then A28: ((len f) -' j) + j = len f by XREAL_1:235;

i < j by A25, NAT_1:13;

then A29: ((len f) -' i) + i = len f by A27, XREAL_1:235, XXREAL_0:2;

then (i + 1) + ((len f) -' i) = (((len f) -' j) + 1) + j by A28;

then (((len f) -' j) + 1) + j < j + ((len f) -' i) by A25, XREAL_1:6;

then A30: ((len f) -' j) + 1 < (len f) -' i by XREAL_1:6;

A31: j + 1 <= len f by A4, A26, NAT_1:13;

per cases
( j + 1 = len f or ( i >= 1 & j + 1 < len f ) or i = 0 )
by A31, NAT_1:14, XXREAL_0:1;

end;

suppose
j + 1 = len f
; :: thesis: LSeg (ff,i) misses LSeg (ff,j)

then
((len f) -' i) + 1 < len f
by A26, A29, FINSEQ_5:def 3, XREAL_1:6;

then LSeg (f,((len f) -' i)) misses LSeg (f,((len f) -' j)) by A30, GOBOARD5:def 4;

then A32: (LSeg (f,((len f) -' i))) /\ (LSeg (f,((len f) -' j))) = {} ;

LSeg (f,((len f) -' i)) = LSeg (ff,i) by A29, SPPOL_2:2;

hence (LSeg (ff,i)) /\ (LSeg (ff,j)) = {} by A28, A32, SPPOL_2:2; :: according to XBOOLE_0:def 7 :: thesis: verum

end;then LSeg (f,((len f) -' i)) misses LSeg (f,((len f) -' j)) by A30, GOBOARD5:def 4;

then A32: (LSeg (f,((len f) -' i))) /\ (LSeg (f,((len f) -' j))) = {} ;

LSeg (f,((len f) -' i)) = LSeg (ff,i) by A29, SPPOL_2:2;

hence (LSeg (ff,i)) /\ (LSeg (ff,j)) = {} by A28, A32, SPPOL_2:2; :: according to XBOOLE_0:def 7 :: thesis: verum

suppose that A33:
i >= 1
and

A34: j + 1 < len f ; :: thesis: LSeg (ff,i) misses LSeg (ff,j)

A34: j + 1 < len f ; :: thesis: LSeg (ff,i) misses LSeg (ff,j)

A35:
(len f) -' j > 1
by A28, A34, XREAL_1:6;

((len f) -' i) + 1 <= len f by A29, A33, XREAL_1:6;

then (len f) -' i < len f by NAT_1:13;

then LSeg (f,((len f) -' i)) misses LSeg (f,((len f) -' j)) by A30, A35, GOBOARD5:def 4;

then A36: (LSeg (f,((len f) -' i))) /\ (LSeg (f,((len f) -' j))) = {} ;

LSeg (f,((len f) -' i)) = LSeg (ff,i) by A29, SPPOL_2:2;

hence (LSeg (ff,i)) /\ (LSeg (ff,j)) = {} by A28, A36, SPPOL_2:2; :: according to XBOOLE_0:def 7 :: thesis: verum

end;((len f) -' i) + 1 <= len f by A29, A33, XREAL_1:6;

then (len f) -' i < len f by NAT_1:13;

then LSeg (f,((len f) -' i)) misses LSeg (f,((len f) -' j)) by A30, A35, GOBOARD5:def 4;

then A36: (LSeg (f,((len f) -' i))) /\ (LSeg (f,((len f) -' j))) = {} ;

LSeg (f,((len f) -' i)) = LSeg (ff,i) by A29, SPPOL_2:2;

hence (LSeg (ff,i)) /\ (LSeg (ff,j)) = {} by A28, A36, SPPOL_2:2; :: according to XBOOLE_0:def 7 :: thesis: verum