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
proof
hereby :: according to GOBOARD5:def 5,GOBOARD1:def 9 :: thesis: for b1 being set holds
( not b1 in dom ff or not b1 + 1 in dom ff or for b2, b3, b4, b5 being set holds
( not [b2,b3] in Indices (GoB ff) or not [b4,b5] in Indices (GoB ff) or not ff /. b1 = (GoB ff) * (b2,b3) or not ff /. (b1 + 1) = (GoB ff) * (b4,b5) or |.(b2 - b4).| + |.(b3 - b5).| = 1 ) )
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;
let k be Nat; :: thesis: ( not k in dom ff or not k + 1 in dom ff or for b1, b2, b3, b4 being set holds
( not [b1,b2] in Indices (GoB ff) or not [b3,b4] in Indices (GoB ff) or not ff /. k = (GoB ff) * (b1,b2) or not ff /. (k + 1) = (GoB ff) * (b3,b4) or |.(b1 - b3).| + |.(b2 - b4).| = 1 ) )
assume that
A11: k in dom ff and
A12: k + 1 in dom ff ; :: thesis: for b1, b2, b3, b4 being set holds
( not [b1,b2] in Indices (GoB ff) or not [b3,b4] in Indices (GoB ff) or not ff /. k = (GoB ff) * (b1,b2) or not ff /. (k + 1) = (GoB ff) * (b3,b4) or |.(b1 - b3).| + |.(b2 - b4).| = 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
.= f /. 1 by FINSEQ_6:def 1
.= ff /. (len ff) by A4, FINSEQ_5:65 ;
ff is s.c.c.
proof
let i be Nat; :: according to GOBOARD5:def 4 :: thesis: for b1 being set holds
( b1 <= i + 1 or ( ( i <= 1 or len ff <= b1 ) & len ff <= b1 + 1 ) or LSeg (ff,i) misses LSeg (ff,b1) )
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;
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;
suppose that A33: i >= 1 and
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;
suppose i = 0 ; :: thesis: LSeg (ff,i) misses LSeg (ff,j)
then LSeg (ff,i) = {} by TOPREAL1:def 3;
hence (LSeg (ff,i)) /\ (LSeg (ff,j)) = {} ; :: according to XBOOLE_0:def 7 :: thesis: verum
end;
end;
end;
hence Rev f is standard special_circular_sequence by A5, A24, FINSEQ_6:def 1, SPPOL_2:28, SPPOL_2:40; :: thesis: verum