reconsider Sb = S-bound D, Nb = N-bound D, Wb = W-bound D, Eb = E-bound D as Element of REAL by XREAL_0:def 1;
A1: <*Sb,Nb*> is increasing

proof

let n, m be Nat; :: according to SEQM_3:def 1 :: thesis:
assume that
A2: n in dom <*Sb,Nb*> and
A3: m in dom <*Sb,Nb*> ; :: thesis:
len <*(S-bound D),(N-bound D)*> = 2 by FINSEQ_1:44;
then A4: dom <*(S-bound D),(N-bound D)*> = {1,2} by FINSEQ_1:2, FINSEQ_1:def 3;
then A5: ( n = 1 or n = 2 ) by A2, TARSKI:def 2;
assume A6: n < m ; :: thesis:
A7: ( m = 1 or m = 2 ) by A4, A3, TARSKI:def 2;
then A8: <*(S-bound D),(N-bound D)*> . m = N-bound D by A5, A6, FINSEQ_1:44;
<*(S-bound D),(N-bound D)*> . n = S-bound D by A5, A7, A6, FINSEQ_1:44;
hence <*Sb,Nb*> . n < <*Sb,Nb*> . m by A8, Th32; :: thesis:

end;

set S = (|[(W-bound D),(S-bound D)]|,|[(W-bound D),(N-bound D)]|) ][ (|[(E-bound D),(S-bound D)]|,|[(E-bound D),(N-bound D)]|);
set Yf1 = <*Nb,Nb,Sb*>;
set Yf2 = <*Sb,Nb*>;
set Xf1 = <*Wb,Eb,Eb*>;
set Xf2 = <*Wb,Wb*>;
set f = SpStSeq D;
set f1 = <*(NW-corner D),(NE-corner D),(SE-corner D)*>;
set f2 = <*(SW-corner D),(NW-corner D)*>;
reconsider Xf = <*Wb,Eb,Eb*> ^ <*Wb,Wb*> as FinSequence of REAL ;
A9: rng <*Wb,Wb*> = {(W-bound D),(W-bound D)} by FINSEQ_2:127
.= {(W-bound D)} by ENUMSET1:29 ;
rng <*Wb,Eb,Eb*> = {(W-bound D),(E-bound D),(E-bound D)} by FINSEQ_2:128
.= {(E-bound D),(E-bound D),(W-bound D)} by ENUMSET1:60
.= {(W-bound D),(E-bound D)} by ENUMSET1:30 ;
then A10: rng Xf = {(W-bound D),(E-bound D)} \/ {(W-bound D)} by A9, FINSEQ_1:31
.= {(W-bound D),(W-bound D),(E-bound D)} by ENUMSET1:2
.= {(W-bound D),(E-bound D)} by ENUMSET1:30 ;
then A11: rng <*(W-bound D),(E-bound D)*> = rng Xf by FINSEQ_2:127;
A12: <*Wb,Eb*> is increasing

proof

let n, m be Nat; :: according to SEQM_3:def 1 :: thesis:
assume that
A13: n in dom <*Wb,Eb*> and
A14: m in dom <*Wb,Eb*> ; :: thesis:
len <*(W-bound D),(E-bound D)*> = 2 by FINSEQ_1:44;
then A15: dom <*(W-bound D),(E-bound D)*> = {1,2} by FINSEQ_1:2, FINSEQ_1:def 3;
then A16: ( n = 1 or n = 2 ) by A13, TARSKI:def 2;
assume A17: n < m ; :: thesis:
A18: ( m = 1 or m = 2 ) by A15, A14, TARSKI:def 2;
then A19: <*(W-bound D),(E-bound D)*> . m = E-bound D by A16, A17, FINSEQ_1:44;
<*(W-bound D),(E-bound D)*> . n = W-bound D by A16, A18, A17, FINSEQ_1:44;
hence <*Wb,Eb*> . n < <*Wb,Eb*> . m by A19, Th31; :: thesis:

end;

proof

let i be Nat; :: according to TOPREAL1:def 5 :: thesis:
assume 1 <= i ; :: thesis:
then 1 + 1 <= i + 1 by XREAL_1:6;
then A41: 1 < i + 1 by XXREAL_0:2;
assume i + 1 <= len (SpStSeq D) ; :: thesis:
then A42: not not i + 1 = 0 & ... & not i + 1 = 5 by A37;

per cases by A41, A42;

suppose A43: i = 1 ; :: thesis:

((SpStSeq D) /. 1) `2 = N-bound D by A33, EUCLID:52
.= ((SpStSeq D) /. (1 + 1)) `2 by A35, EUCLID:52 ;
hence ( ((SpStSeq D) /. i) `1 = ((SpStSeq D) /. (i + 1)) `1 or ((SpStSeq D) /. i) `2 = ((SpStSeq D) /. (i + 1)) `2 ) by A43; :: thesis:

end;

suppose A44: i = 2 ; :: thesis:

((SpStSeq D) /. 2) `1 = E-bound D by A35, EUCLID:52
.= ((SpStSeq D) /. (2 + 1)) `1 by A34, EUCLID:52 ;
hence ( ((SpStSeq D) /. i) `1 = ((SpStSeq D) /. (i + 1)) `1 or ((SpStSeq D) /. i) `2 = ((SpStSeq D) /. (i + 1)) `2 ) by A44; :: thesis:

end;

suppose A45: i = 3 ; :: thesis:

((SpStSeq D) /. 3) `2 = S-bound D by A34, EUCLID:52
.= ((SpStSeq D) /. (3 + 1)) `2 by A38, EUCLID:52 ;
hence ( ((SpStSeq D) /. i) `1 = ((SpStSeq D) /. (i + 1)) `1 or ((SpStSeq D) /. i) `2 = ((SpStSeq D) /. (i + 1)) `2 ) by A45; :: thesis:

end;

suppose A46: i = 4 ; :: thesis:

((SpStSeq D) /. 4) `1 = W-bound D by A38, EUCLID:52
.= ((SpStSeq D) /. (4 + 1)) `1 by A40, EUCLID:52 ;
hence ( ((SpStSeq D) /. i) `1 = ((SpStSeq D) /. (i + 1)) `1 or ((SpStSeq D) /. i) `2 = ((SpStSeq D) /. (i + 1)) `2 ) by A46; :: thesis:

end;

4 + 1 = 5 ;
then A47: LSeg ((SpStSeq D),4) = LSeg ((SW-corner D),(NW-corner D)) by A37, A38, A40, TOPREAL1:def 3;
2 + 1 = 3 ;
then A48: LSeg ((SpStSeq D),2) = LSeg ((NE-corner D),(SE-corner D)) by A37, A35, A34, TOPREAL1:def 3;
1 in dom <*Sb,Nb*> by A27, FINSEQ_3:25;
then A49: Yf . (3 + 1) = <*Sb,Nb*> . 1 by A25, FINSEQ_1:def 7
.= S-bound D by FINSEQ_1:44 ;

now :: thesis:

let n be Nat; :: thesis:
assume A50: n in dom Yf ; :: thesis:
then A51: n <> 0 by FINSEQ_3:25;
n <= 5 by A28, A50, FINSEQ_3:25;
then not not n = 0 & ... & not n = 5 ;

per cases by A51;

suppose n = 1 ; :: thesis:

hence Yf . n = ((SpStSeq D) /. n) `2 by A33, A26, EUCLID:52; :: thesis:

end;

suppose n = 2 ; :: thesis:

hence Yf . n = ((SpStSeq D) /. n) `2 by A35, A31, EUCLID:52; :: thesis:

end;

suppose n = 3 ; :: thesis:

hence Yf . n = ((SpStSeq D) /. n) `2 by A34, A30, EUCLID:52; :: thesis:

end;

suppose n = 4 ; :: thesis:

hence Yf . n = ((SpStSeq D) /. n) `2 by A38, A49, EUCLID:52; :: thesis:

end;

suppose n = 5 ; :: thesis:

hence Yf . n = ((SpStSeq D) /. n) `2 by A40, A29, EUCLID:52; :: thesis:

end;

then Yf = Y_axis (SpStSeq D) by A37, A28, GOBOARD1:def 2;
then A52: <*(S-bound D),(N-bound D)*> = Incr (Y_axis (SpStSeq D)) by A23, A24, A1, SEQ_4:def 21;
1 + 1 = 2 ;
then A53: LSeg ((SpStSeq D),1) = LSeg ((NW-corner D),(NE-corner D)) by A37, A33, A35, TOPREAL1:def 3;
thus SpStSeq D is unfolded :: thesis:

proof

let i be Nat; :: according to TOPREAL1:def 6 :: thesis:
assume 1 <= i ; :: thesis:
then A54: 1 + 2 <= i + 2 by XREAL_1:6;
assume A55: i + 2 <= len (SpStSeq D) ; :: thesis:
A56: 2 < i + 2 by A54, XXREAL_0:2;
not not i + 2 = 0 & ... & not i + 2 = 5 by A37, A55;

per cases by A56;

suppose i = 1 ; :: thesis:

hence (LSeg ((SpStSeq D),i)) /\ (LSeg ((SpStSeq D),(i + 1))) = {((SpStSeq D) /. (i + 1))} by A35, A53, A48, Th28; :: thesis:

end;

suppose i = 2 ; :: thesis:

hence (LSeg ((SpStSeq D),i)) /\ (LSeg ((SpStSeq D),(i + 1))) = {((SpStSeq D) /. (i + 1))} by A34, A48, A39, Th29; :: thesis:

end;

suppose i = 3 ; :: thesis:

hence (LSeg ((SpStSeq D),i)) /\ (LSeg ((SpStSeq D),(i + 1))) = {((SpStSeq D) /. (i + 1))} by A38, A39, A47, Th30; :: thesis:

end;

thus SpStSeq D is circular by A37, A33, A40, FINSEQ_6:def 1; :: thesis:
thus SpStSeq D is s.c.c. :: thesis:

proof

let i be Nat; :: according to GOBOARD5:def 4 :: thesis:
let j be Nat; :: thesis:
assume that
A57: i + 1 < j and
A58: ( ( i > 1 & j < len (SpStSeq D) ) or j + 1 < len (SpStSeq D) ) ; :: thesis:
j + 1 <= 5 by A37, A58, NAT_1:13;
then A59: not not j + 1 = 0 & ... & not j + 1 = 5 ;
A60: (i + 1) + 1 = i + (1 + 1) ;
then A61: i + 2 <> 0 + 1 ;
A62: i + 2 <= j by A57, A60, NAT_1:13;

A63: now :: thesis:

per cases by A57, A59, NAT_1:11;

case j = 2 ; :: thesis:

then i + 2 <= 2 by A62;
then not not i + 2 = 0 & ... & not i + 2 = 2 ;
hence i = 0 by A57; :: thesis:

end;

case j = 3 ; :: thesis:

then i + 2 <= 3 by A62;
then not not i + 2 = 0 & ... & not i + 2 = 3 ;
hence ( i = 0 or i = 1 ) by A57; :: thesis:

end;

case A64: j = 4 ; :: thesis:

then i + 2 <= 4 by A62;
then not not i + 2 = 0 & ... & not i + 2 = 4 ;
hence ( i = 0 or i = 2 ) by A37, A58, A61, A64; :: thesis:

end;

per cases by A63;

suppose i = 0 ; :: thesis:

then LSeg ((SpStSeq D),i) = {} by TOPREAL1:def 3;
hence (LSeg ((SpStSeq D),i)) /\ (LSeg ((SpStSeq D),j)) = {} ; :: according to XBOOLE_0:def 7 :: thesis:

end;

suppose ( i = 1 & j = 3 ) ; :: thesis:

then LSeg ((SpStSeq D),i) misses LSeg ((SpStSeq D),j) by A53, A39, Th34;
hence (LSeg ((SpStSeq D),i)) /\ (LSeg ((SpStSeq D),j)) = {} ; :: according to XBOOLE_0:def 7 :: thesis:

end;

suppose ( i = 2 & j = 4 ) ; :: thesis:

then LSeg ((SpStSeq D),i) misses LSeg ((SpStSeq D),j) by A48, A47, Th33;
hence (LSeg ((SpStSeq D),i)) /\ (LSeg ((SpStSeq D),j)) = {} ; :: according to XBOOLE_0:def 7 :: thesis:

end;

A65: W-bound D < E-bound D by Th31;
A66: len <*(W-bound D),(E-bound D)*> = 2 by FINSEQ_1:44
.= card (rng Xf) by A65, A10, CARD_2:57 ;
A67: len <*Wb,Eb,Eb*> = 3 by FINSEQ_1:45;
then 1 in dom <*Wb,Eb,Eb*> by FINSEQ_3:25;
then A68: Xf . 1 = <*Wb,Eb,Eb*> . 1 by FINSEQ_1:def 7
.= W-bound D by FINSEQ_1:45 ;
A69: len <*Wb,Wb*> = 2 by FINSEQ_1:44;
then A70: len Xf = 3 + 2 by A67, FINSEQ_1:22;
2 in dom <*Wb,Wb*> by A69, FINSEQ_3:25;
then A71: Xf . (3 + 2) = <*Wb,Wb*> . 2 by A67, FINSEQ_1:def 7
.= W-bound D by FINSEQ_1:44 ;
3 in dom <*Wb,Eb,Eb*> by A67, FINSEQ_3:25;
then A72: Xf . 3 = <*Wb,Eb,Eb*> . 3 by FINSEQ_1:def 7
.= E-bound D by FINSEQ_1:45 ;
2 in dom <*Wb,Eb,Eb*> by A67, FINSEQ_3:25;
then A73: Xf . 2 = <*Wb,Eb,Eb*> . 2 by FINSEQ_1:def 7
.= E-bound D by FINSEQ_1:45 ;
1 in dom <*Wb,Wb*> by A69, FINSEQ_3:25;
then A74: Xf . (3 + 1) = <*Wb,Wb*> . 1 by A67, FINSEQ_1:def 7
.= W-bound D by FINSEQ_1:44 ;

now :: thesis:

let n be Nat; :: thesis:
assume A75: n in dom Xf ; :: thesis:
then A76: n <> 0 by FINSEQ_3:25;
n <= 5 by A70, A75, FINSEQ_3:25;
then not not n = 0 & ... & not n = 5 ;

per cases by A76;

suppose n = 1 ; :: thesis:

hence Xf . n = ((SpStSeq D) /. n) `1 by A33, A68, EUCLID:52; :: thesis:

end;

suppose n = 2 ; :: thesis:

hence Xf . n = ((SpStSeq D) /. n) `1 by A35, A73, EUCLID:52; :: thesis:

end;

suppose n = 3 ; :: thesis:

hence Xf . n = ((SpStSeq D) /. n) `1 by A34, A72, EUCLID:52; :: thesis:

end;

suppose n = 4 ; :: thesis:

hence Xf . n = ((SpStSeq D) /. n) `1 by A38, A74, EUCLID:52; :: thesis:

end;

suppose n = 5 ; :: thesis:

hence Xf . n = ((SpStSeq D) /. n) `1 by A40, A71, EUCLID:52; :: thesis:

end;

proof

let n, m be Nat; :: thesis:
A79: <*(S-bound D),(N-bound D)*> . 1 = S-bound D by FINSEQ_1:44;
assume [n,m] in Indices ((|[(W-bound D),(S-bound D)]|,|[(W-bound D),(N-bound D)]|) ][ (|[(E-bound D),(S-bound D)]|,|[(E-bound D),(N-bound D)]|)) ; :: thesis:
then [n,m] in [:{1,2},{1,2}:] by FINSEQ_1:2, MATRIX_0:47;
then A80: [n,m] in {[1,1],[1,2],[2,1],[2,2]} by MCART_1:23;
A81: <*(S-bound D),(N-bound D)*> . 2 = N-bound D by FINSEQ_1:44;

per cases = [1,1] or [n,m] = [1,2] or [n,m] = [2,1] or [n,m] = [2,2] ) by A80, ENUMSET1:def 2;

suppose A82: [n,m] = [1,1] ; :: thesis:

end;

suppose A85: [n,m] = [1,2] ; :: thesis:

end;

suppose A88: [n,m] = [2,1] ; :: thesis:

end;

suppose A91: [n,m] = [2,2] ; :: thesis:

end;

proof

thus for k being Nat st k in dom (SpStSeq D) holds
ex i, j being Nat st
( [i,j] in Indices (GoB (SpStSeq D)) & (SpStSeq D) /. k = (GoB (SpStSeq D)) * (i,j) ) :: according to GOBOARD1:def 9,GOBOARD5:def 5 :: thesis:

proof

let k be Nat; :: thesis:
assume A100: k in dom (SpStSeq D) ; :: thesis:
then A101: k >= 1 by FINSEQ_3:25;
k <= 5 by A37, A100, FINSEQ_3:25;
then not not k = 0 & ... & not k = 5 ;

per cases by A101;

suppose A102: k = 1 ; :: thesis:

take 1 ; :: thesis:
take 2 ; :: thesis:
thus [1,2] in Indices (GoB (SpStSeq D)) by A95, MATRIX_0:48; :: thesis:
thus (SpStSeq D) /. k = (GoB (SpStSeq D)) * (1,2) by A33, A95, A102, MATRIX_0:50; :: thesis:

end;

suppose A103: k = 2 ; :: thesis:

take 2 ; :: thesis:
take 2 ; :: thesis:
thus [2,2] in Indices (GoB (SpStSeq D)) by A95, MATRIX_0:48; :: thesis:
thus (SpStSeq D) /. k = (GoB (SpStSeq D)) * (2,2) by A35, A95, A103, MATRIX_0:50; :: thesis:

end;

suppose A104: k = 3 ; :: thesis:

take 2 ; :: thesis:
take 1 ; :: thesis:
thus [2,1] in Indices (GoB (SpStSeq D)) by A95, MATRIX_0:48; :: thesis:
thus (SpStSeq D) /. k = (GoB (SpStSeq D)) * (2,1) by A34, A95, A104, MATRIX_0:50; :: thesis:

end;

suppose A105: k = 4 ; :: thesis:

take 1 ; :: thesis:
take 1 ; :: thesis:
thus [1,1] in Indices (GoB (SpStSeq D)) by A95, MATRIX_0:48; :: thesis:
thus (SpStSeq D) /. k = (GoB (SpStSeq D)) * (1,1) by A38, A95, A105, MATRIX_0:50; :: thesis:

end;

suppose A106: k = 5 ; :: thesis:

take 1 ; :: thesis:
take 2 ; :: thesis:
thus [1,2] in Indices (GoB (SpStSeq D)) by A95, MATRIX_0:48; :: thesis:
thus (SpStSeq D) /. k = (GoB (SpStSeq D)) * (1,2) by A40, A95, A106, MATRIX_0:50; :: thesis:

end;

let n be Nat; :: thesis:
assume that
A107: n in dom (SpStSeq D) and
A108: n + 1 in dom (SpStSeq D) ; :: thesis:
A109: n <> 0 by A107, FINSEQ_3:25;
n + 1 <= 4 + 1 by A37, A108, FINSEQ_3:25;
then A110: n <= 4 by XREAL_1:6;
let m, k, i, j be Nat; :: thesis:
assume that
A111: [m,k] in Indices (GoB (SpStSeq D)) and
A112: [i,j] in Indices (GoB (SpStSeq D)) and
A113: (SpStSeq D) /. n = (GoB (SpStSeq D)) * (m,k) and
A114: (SpStSeq D) /. (n + 1) = (GoB (SpStSeq D)) * (i,j) ; :: thesis:
not not n = 0 & ... & not n = 4 by A110;

per cases by A109;

suppose A115: n = 1 ; :: thesis:

A116: [2,2] in Indices (GoB (SpStSeq D)) by A95, MATRIX_0:48;
then A117: i = 1 + 1 by A96, A112, A114, A115, GOBOARD1:5;
A118: [1,2] in Indices (GoB (SpStSeq D)) by A95, MATRIX_0:48;
then m = 1 by A99, A111, A113, A115, GOBOARD1:5;
then A119: |.(m - i).| = 1 by A117, SEQM_3:41;
A120: j = 2 by A96, A112, A114, A115, A116, GOBOARD1:5;
k = 2 by A99, A111, A113, A115, A118, GOBOARD1:5;
hence |.(m - i).| + |.(k - j).| = 1 by A120, A119, SEQM_3:42; :: thesis:

end;

suppose A121: n = 2 ; :: thesis:

A122: [2,1] in Indices (GoB (SpStSeq D)) by A95, MATRIX_0:48;
then A123: j = 1 by A98, A112, A114, A121, GOBOARD1:5;
A124: [2,2] in Indices (GoB (SpStSeq D)) by A95, MATRIX_0:48;
then k = 1 + 1 by A96, A111, A113, A121, GOBOARD1:5;
then A125: |.(k - j).| = 1 by A123, SEQM_3:41;
A126: i = 2 by A98, A112, A114, A121, A122, GOBOARD1:5;
m = 2 by A96, A111, A113, A121, A124, GOBOARD1:5;
hence |.(m - i).| + |.(k - j).| = 1 by A126, A125, SEQM_3:42; :: thesis:

end;

suppose A127: n = 3 ; :: thesis:

A128: [1,1] in Indices (GoB (SpStSeq D)) by A95, MATRIX_0:48;
then A129: i = 1 by A97, A112, A114, A127, GOBOARD1:5;
A130: [2,1] in Indices (GoB (SpStSeq D)) by A95, MATRIX_0:48;
then m = 1 + 1 by A98, A111, A113, A127, GOBOARD1:5;
then A131: |.(m - i).| = 1 by A129, SEQM_3:41;
A132: j = 1 by A97, A112, A114, A127, A128, GOBOARD1:5;
k = 1 by A98, A111, A113, A127, A130, GOBOARD1:5;
hence |.(m - i).| + |.(k - j).| = 1 by A132, A131, SEQM_3:42; :: thesis:

end;

suppose A133: n = 4 ; :: thesis:

A134: [1,1] in Indices (GoB (SpStSeq D)) by A95, MATRIX_0:48;
then A135: k = 1 by A97, A111, A113, A133, GOBOARD1:5;
A136: [1,2] in Indices (GoB (SpStSeq D)) by A95, MATRIX_0:48;
then j = 1 + 1 by A33, A40, A99, A112, A114, A133, GOBOARD1:5;
then A137: |.(k - j).| = 1 by A135, SEQM_3:41;
A138: m = 1 by A97, A111, A113, A133, A134, GOBOARD1:5;
i = 1 by A33, A40, A99, A112, A114, A133, A136, GOBOARD1:5;
hence |.(m - i).| + |.(k - j).| = 1 by A138, A137, SEQM_3:42; :: thesis:

end;