set f1 = <*(NW-corner D),(NE-corner D),(SE-corner D)*>;
set f2 = <*(SW-corner D),(NW-corner D)*>;
A1: ( len <*(NW-corner D),(NE-corner D),(SE-corner D)*> = 3 & len <*(SW-corner D),(NW-corner D)*> = 2 ) by FINSEQ_1:61, FINSEQ_1:62;
then A2: len (<*(NW-corner D),(NE-corner D),(SE-corner D)*> ^ <*(SW-corner D),(NW-corner D)*>) = 3 + 2 by FINSEQ_1:35;
set f = SpStSeq D;
1 in dom <*(NW-corner D),(NE-corner D),(SE-corner D)*> by A1, FINSEQ_3:27;
then A3: (SpStSeq D) /. 1 = <*(NW-corner D),(NE-corner D),(SE-corner D)*> /. 1 by FINSEQ_4:83
.= NW-corner D by FINSEQ_4:27 ;
2 in dom <*(NW-corner D),(NE-corner D),(SE-corner D)*> by A1, FINSEQ_3:27;
then A4: (SpStSeq D) /. 2 = <*(NW-corner D),(NE-corner D),(SE-corner D)*> /. 2 by FINSEQ_4:83
.= NE-corner D by FINSEQ_4:27 ;
3 in dom <*(NW-corner D),(NE-corner D),(SE-corner D)*> by A1, FINSEQ_3:27;
then A5: (SpStSeq D) /. 3 = <*(NW-corner D),(NE-corner D),(SE-corner D)*> /. 3 by FINSEQ_4:83
.= SE-corner D by FINSEQ_4:27 ;
1 in dom <*(SW-corner D),(NW-corner D)*> by A1, FINSEQ_3:27;
then A6: (SpStSeq D) /. (3 + 1) = <*(SW-corner D),(NW-corner D)*> /. 1 by A1, FINSEQ_4:84
.= SW-corner D by FINSEQ_4:26 ;
2 in dom <*(SW-corner D),(NW-corner D)*> by A1, FINSEQ_3:27;
then A7: (SpStSeq D) /. (3 + 2) = <*(SW-corner D),(NW-corner D)*> /. 2 by A1, FINSEQ_4:84
.= NW-corner D by FINSEQ_4:26 ;
1 + 1 = 2 ;
then A8: LSeg (SpStSeq D),1 = LSeg (NW-corner D),(NE-corner D) by A2, A3, A4, TOPREAL1:def 5;
2 + 1 = 3 ;
then A9: LSeg (SpStSeq D),2 = LSeg (NE-corner D),(SE-corner D) by A2, A4, A5, TOPREAL1:def 5;
A10: LSeg (SpStSeq D),3 = LSeg (SE-corner D),(SW-corner D) by A2, A5, A6, TOPREAL1:def 5;
4 + 1 = 5 ;
then A11: LSeg (SpStSeq D),4 = LSeg (SW-corner D),(NW-corner D) by A2, A6, A7, TOPREAL1:def 5;
thus SpStSeq D is special :: thesis:

proof

let i be Nat; :: according to TOPREAL1:def 7 :: thesis:
assume 1 <= i ; :: thesis:
then 1 + 1 <= i + 1 by XREAL_1:8;
then A12: ( 1 < i + 1 & 0 < i + 1 ) by XXREAL_0:2;
assume i + 1 <= len (SpStSeq D) ; :: thesis:
then A13: ( i + 1 = 1 + 1 or i + 1 = 2 + 1 or i + 1 = 3 + 1 or i + 1 = 4 + 1 ) by A2, A12, NAT_1:30;

per cases by A13;

suppose A14: i = 1 ; :: thesis:

((SpStSeq D) /. 1) `2 = N-bound D by A3, EUCLID:56
.= ((SpStSeq D) /. (1 + 1)) `2 by A4, EUCLID:56 ;
hence ( ((SpStSeq D) /. i) `1 = ((SpStSeq D) /. (i + 1)) `1 or ((SpStSeq D) /. i) `2 = ((SpStSeq D) /. (i + 1)) `2 ) by A14; :: thesis:

end;

suppose A15: i = 2 ; :: thesis:

((SpStSeq D) /. 2) `1 = E-bound D by A4, EUCLID:56
.= ((SpStSeq D) /. (2 + 1)) `1 by A5, EUCLID:56 ;
hence ( ((SpStSeq D) /. i) `1 = ((SpStSeq D) /. (i + 1)) `1 or ((SpStSeq D) /. i) `2 = ((SpStSeq D) /. (i + 1)) `2 ) by A15; :: thesis:

end;

suppose A16: i = 3 ; :: thesis:

((SpStSeq D) /. 3) `2 = S-bound D by A5, EUCLID:56
.= ((SpStSeq D) /. (3 + 1)) `2 by A6, EUCLID:56 ;
hence ( ((SpStSeq D) /. i) `1 = ((SpStSeq D) /. (i + 1)) `1 or ((SpStSeq D) /. i) `2 = ((SpStSeq D) /. (i + 1)) `2 ) by A16; :: thesis:

end;

suppose A17: i = 4 ; :: thesis:

((SpStSeq D) /. 4) `1 = W-bound D by A6, EUCLID:56
.= ((SpStSeq D) /. (4 + 1)) `1 by A7, EUCLID:56 ;
hence ( ((SpStSeq D) /. i) `1 = ((SpStSeq D) /. (i + 1)) `1 or ((SpStSeq D) /. i) `2 = ((SpStSeq D) /. (i + 1)) `2 ) by A17; :: thesis:

end;

thus SpStSeq D is unfolded :: thesis:

proof

let i be Nat; :: according to TOPREAL1:def 8 :: thesis:
assume 1 <= i ; :: thesis:
then 1 + 2 <= i + 2 by XREAL_1:8;
then A18: ( 2 < i + 2 & 1 < i + 2 & 0 < i + 2 ) by XXREAL_0:2;
assume i + 2 <= len (SpStSeq D) ; :: thesis:
then A19: ( i + 2 = 1 + 2 or i + 2 = 2 + 2 or i + 2 = 3 + 2 ) by A2, A18, NAT_1:30;

per cases by A19;

suppose i = 1 ; :: thesis:

hence (LSeg (SpStSeq D),i) /\ (LSeg (SpStSeq D),(i + 1)) = {((SpStSeq D) /. (i + 1))} by A4, A8, A9, Th30; :: thesis:

end;

suppose i = 2 ; :: thesis:

hence (LSeg (SpStSeq D),i) /\ (LSeg (SpStSeq D),(i + 1)) = {((SpStSeq D) /. (i + 1))} by A5, A9, A10, Th31; :: thesis:

end;

suppose i = 3 ; :: thesis:

hence (LSeg (SpStSeq D),i) /\ (LSeg (SpStSeq D),(i + 1)) = {((SpStSeq D) /. (i + 1))} by A6, A10, A11, Th32; :: thesis:

end;

thus SpStSeq D is circular by A2, A3, A7, FINSEQ_6:def 1; :: thesis:
thus SpStSeq D is s.c.c. :: thesis:

proof

let i be Element of NAT ; :: according to GOBOARD5:def 4 :: thesis:
let j be Element of NAT ; :: thesis:
assume that
A20: i + 1 < j and
A21: ( ( i > 1 & j < len (SpStSeq D) ) or j + 1 < len (SpStSeq D) ) ; :: thesis:
A22: ( j + 1 = 0 + 1 or j + 1 = 1 + 1 or j + 1 = 2 + 1 or j + 1 = 3 + 1 or j + 1 = 4 + 1 ) by A2, A21, NAT_1:30;
A23: (i + 1) + 1 = i + (1 + 1) ;
then A24: i + 2 <= j by A20, NAT_1:13;
A25: ( ( i + 2 = 2 + 2 implies i = 2 ) & ( i + 2 = 1 + 2 implies i = 1 ) & ( i + 2 = 0 + 2 implies i = 0 ) ) ;
A26: i + 2 <> 0 + 1 by A23;

A27: now

per cases by A20, A22, NAT_1:11;

case j = 2 ; :: thesis:

hence i = 0 by A20, A23, A25, NAT_1:27; :: thesis:

end;

case j = 3 ; :: thesis:

hence ( i = 0 or i = 1 ) by A20, A23, A25, NAT_1:28; :: thesis:

end;

case j = 4 ; :: thesis:

hence ( i = 0 or i = 2 ) by A2, A21, A24, A25, A26, NAT_1:29; :: thesis:

end;

per cases by A27;

suppose i = 0 ; :: thesis:

then LSeg (SpStSeq D),i = {} by TOPREAL1:def 5;
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 A8, A10, Th36;
hence (LSeg (SpStSeq D),i) /\ (LSeg (SpStSeq D),j) = {} by XBOOLE_0:def 7; :: 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 A9, A11, Th35;
hence (LSeg (SpStSeq D),i) /\ (LSeg (SpStSeq D),j) = {} by XBOOLE_0:def 7; :: according to XBOOLE_0:def 7 :: thesis:

end;

set Xf1 = <*(W-bound D),(E-bound D),(E-bound D)*>;
set Xf2 = <*(W-bound D),(W-bound D)*>;
reconsider Xf = <*(W-bound D),(E-bound D),(E-bound D)*> ^ <*(W-bound D),(W-bound D)*> as FinSequence of REAL ;
A28: ( len <*(W-bound D),(E-bound D),(E-bound D)*> = 3 & len <*(W-bound D),(W-bound D)*> = 2 ) by FINSEQ_1:61, FINSEQ_1:62;
then A29: len Xf = 3 + 2 by FINSEQ_1:35;
1 in dom <*(W-bound D),(E-bound D),(E-bound D)*> by A28, FINSEQ_3:27;
then A30: Xf . 1 = <*(W-bound D),(E-bound D),(E-bound D)*> . 1 by FINSEQ_1:def 7
.= W-bound D by FINSEQ_1:62 ;
2 in dom <*(W-bound D),(E-bound D),(E-bound D)*> by A28, FINSEQ_3:27;
then A31: Xf . 2 = <*(W-bound D),(E-bound D),(E-bound D)*> . 2 by FINSEQ_1:def 7
.= E-bound D by FINSEQ_1:62 ;
3 in dom <*(W-bound D),(E-bound D),(E-bound D)*> by A28, FINSEQ_3:27;
then A32: Xf . 3 = <*(W-bound D),(E-bound D),(E-bound D)*> . 3 by FINSEQ_1:def 7
.= E-bound D by FINSEQ_1:62 ;
1 in dom <*(W-bound D),(W-bound D)*> by A28, FINSEQ_3:27;
then A33: Xf . (3 + 1) = <*(W-bound D),(W-bound D)*> . 1 by A28, FINSEQ_1:def 7
.= W-bound D by FINSEQ_1:61 ;
2 in dom <*(W-bound D),(W-bound D)*> by A28, FINSEQ_3:27;
then A34: Xf . (3 + 2) = <*(W-bound D),(W-bound D)*> . 2 by A28, FINSEQ_1:def 7
.= W-bound D by FINSEQ_1:61 ;

now

let n be Element of NAT ; :: thesis:
assume n in dom Xf ; :: thesis:
then A35: ( n <> 0 & n <= 5 ) by A29, FINSEQ_3:27;

per cases by A35, NAT_1:30;

suppose n = 1 ; :: thesis:

hence Xf . n = ((SpStSeq D) /. n) `1 by A3, A30, EUCLID:56; :: thesis:

end;

suppose n = 2 ; :: thesis:

hence Xf . n = ((SpStSeq D) /. n) `1 by A4, A31, EUCLID:56; :: thesis:

end;

suppose n = 3 ; :: thesis:

hence Xf . n = ((SpStSeq D) /. n) `1 by A5, A32, EUCLID:56; :: thesis:

end;

suppose n = 4 ; :: thesis:

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

end;

suppose n = 5 ; :: thesis:

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

end;

then A36: Xf = X_axis (SpStSeq D) by A2, A29, GOBOARD1:def 3;
A37: W-bound D < E-bound D by Th33;
A38: rng <*(W-bound D),(E-bound D),(E-bound D)*> = {(W-bound D),(E-bound D),(E-bound D)} by FINSEQ_2:148
.= {(E-bound D),(E-bound D),(W-bound D)} by ENUMSET1:102
.= {(W-bound D),(E-bound D)} by ENUMSET1:70 ;
rng <*(W-bound D),(W-bound D)*> = {(W-bound D),(W-bound D)} by FINSEQ_2:147
.= {(W-bound D)} by ENUMSET1:69 ;
then A39: rng Xf = {(W-bound D),(E-bound D)} \/ {(W-bound D)} by A38, FINSEQ_1:44
.= {(W-bound D),(W-bound D),(E-bound D)} by ENUMSET1:42
.= {(W-bound D),(E-bound D)} by ENUMSET1:70 ;
then A40: rng <*(W-bound D),(E-bound D)*> = rng Xf by FINSEQ_2:147;
A41: len <*(W-bound D),(E-bound D)*> = 2 by FINSEQ_1:61
.= card (rng Xf) by A37, A39, CARD_2:76 ;
<*(W-bound D),(E-bound D)*> is increasing

proof

let n, m be Element of NAT ; :: according to SEQM_3:def 1 :: thesis:
len <*(W-bound D),(E-bound D)*> = 2 by FINSEQ_1:61;
then A42: dom <*(W-bound D),(E-bound D)*> = {1,2} by FINSEQ_1:4, FINSEQ_1:def 3;
assume ( n in dom <*(W-bound D),(E-bound D)*> & m in dom <*(W-bound D),(E-bound D)*> ) ; :: thesis:
then A43: ( ( n = 1 or n = 2 ) & ( m = 1 or m = 2 ) ) by A42, TARSKI:def 2;
assume n < m ; :: thesis:
then ( <*(W-bound D),(E-bound D)*> . n = W-bound D & <*(W-bound D),(E-bound D)*> . m = E-bound D ) by A43, FINSEQ_1:61;
hence <*(W-bound D),(E-bound D)*> . n < <*(W-bound D),(E-bound D)*> . m by Th33; :: thesis:

end;

then A44: <*(W-bound D),(E-bound D)*> = Incr (X_axis (SpStSeq D)) by A36, A40, A41, GOBOARD2:def 2;
set Yf1 = <*(N-bound D),(N-bound D),(S-bound D)*>;
set Yf2 = <*(S-bound D),(N-bound D)*>;
A45: S-bound D < N-bound D by Th34;
reconsider Yf = <*(N-bound D),(N-bound D),(S-bound D)*> ^ <*(S-bound D),(N-bound D)*> as FinSequence of REAL ;
A46: ( len <*(N-bound D),(N-bound D),(S-bound D)*> = 3 & len <*(S-bound D),(N-bound D)*> = 2 ) by FINSEQ_1:61, FINSEQ_1:62;
then A47: len Yf = 3 + 2 by FINSEQ_1:35;
1 in dom <*(N-bound D),(N-bound D),(S-bound D)*> by A46, FINSEQ_3:27;
then A48: Yf . 1 = <*(N-bound D),(N-bound D),(S-bound D)*> . 1 by FINSEQ_1:def 7
.= N-bound D by FINSEQ_1:62 ;
2 in dom <*(N-bound D),(N-bound D),(S-bound D)*> by A46, FINSEQ_3:27;
then A49: Yf . 2 = <*(N-bound D),(N-bound D),(S-bound D)*> . 2 by FINSEQ_1:def 7
.= N-bound D by FINSEQ_1:62 ;
3 in dom <*(N-bound D),(N-bound D),(S-bound D)*> by A46, FINSEQ_3:27;
then A50: Yf . 3 = <*(N-bound D),(N-bound D),(S-bound D)*> . 3 by FINSEQ_1:def 7
.= S-bound D by FINSEQ_1:62 ;
1 in dom <*(S-bound D),(N-bound D)*> by A46, FINSEQ_3:27;
then A51: Yf . (3 + 1) = <*(S-bound D),(N-bound D)*> . 1 by A46, FINSEQ_1:def 7
.= S-bound D by FINSEQ_1:61 ;
2 in dom <*(S-bound D),(N-bound D)*> by A46, FINSEQ_3:27;
then A52: Yf . (3 + 2) = <*(S-bound D),(N-bound D)*> . 2 by A46, FINSEQ_1:def 7
.= N-bound D by FINSEQ_1:61 ;

now

let n be Element of NAT ; :: thesis:
assume n in dom Yf ; :: thesis:
then A53: ( n <> 0 & n <= 5 ) by A47, FINSEQ_3:27;

per cases by A53, NAT_1:30;

suppose n = 1 ; :: thesis:

hence Yf . n = ((SpStSeq D) /. n) `2 by A3, A48, EUCLID:56; :: thesis:

end;

suppose n = 2 ; :: thesis:

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

end;

suppose n = 3 ; :: thesis:

hence Yf . n = ((SpStSeq D) /. n) `2 by A5, A50, EUCLID:56; :: thesis:

end;

suppose n = 4 ; :: thesis:

hence Yf . n = ((SpStSeq D) /. n) `2 by A6, A51, EUCLID:56; :: thesis:

end;

suppose n = 5 ; :: thesis:

hence Yf . n = ((SpStSeq D) /. n) `2 by A7, A52, EUCLID:56; :: thesis:

end;

then A54: Yf = Y_axis (SpStSeq D) by A2, A47, GOBOARD1:def 4;
A55: rng <*(N-bound D),(N-bound D),(S-bound D)*> = {(N-bound D),(N-bound D),(S-bound D)} by FINSEQ_2:148
.= {(S-bound D),(N-bound D)} by ENUMSET1:70 ;
rng <*(S-bound D),(N-bound D)*> = {(S-bound D),(N-bound D)} by FINSEQ_2:147;
then A56: rng Yf = {(S-bound D),(N-bound D)} \/ {(S-bound D),(N-bound D)} by A55, FINSEQ_1:44
.= {(S-bound D),(N-bound D)} ;
then A57: rng <*(S-bound D),(N-bound D)*> = rng Yf by FINSEQ_2:147;
A58: len <*(S-bound D),(N-bound D)*> = 2 by FINSEQ_1:61
.= card (rng Yf) by A45, A56, CARD_2:76 ;
<*(S-bound D),(N-bound D)*> is increasing

proof

let n, m be Element of NAT ; :: according to SEQM_3:def 1 :: thesis:
len <*(S-bound D),(N-bound D)*> = 2 by FINSEQ_1:61;
then A59: dom <*(S-bound D),(N-bound D)*> = {1,2} by FINSEQ_1:4, FINSEQ_1:def 3;
assume ( n in dom <*(S-bound D),(N-bound D)*> & m in dom <*(S-bound D),(N-bound D)*> ) ; :: thesis:
then A60: ( ( n = 1 or n = 2 ) & ( m = 1 or m = 2 ) ) by A59, TARSKI:def 2;
assume n < m ; :: thesis:
then ( <*(S-bound D),(N-bound D)*> . n = S-bound D & <*(S-bound D),(N-bound D)*> . m = N-bound D ) by A60, FINSEQ_1:61;
hence <*(S-bound D),(N-bound D)*> . n < <*(S-bound D),(N-bound D)*> . m by Th34; :: thesis:

end;

proof

let n, m be Element of NAT ; :: thesis:
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:4, MATRIX_2:3;
then A64: [n,m] in {[1,1],[1,2],[2,1],[2,2]} by MCART_1:25;
A65: ( <*(S-bound D),(N-bound D)*> . 1 = S-bound D & <*(S-bound D),(N-bound D)*> . 2 = N-bound D ) by FINSEQ_1:61;

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

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

end;

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

end;

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

end;

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

end;

then A70: |[(W-bound D),(S-bound D)]|,|[(W-bound D),(N-bound D)]| ][ |[(E-bound D),(S-bound D)]|,|[(E-bound D),(N-bound D)]| = GoB (Incr (X_axis (SpStSeq D))),(Incr (Y_axis (SpStSeq D))) by A62, A63, GOBOARD2:def 1
.= GoB (SpStSeq D) by GOBOARD2:def 3 ;
then A71: (SpStSeq D) /. 1 = (GoB (SpStSeq D)) * 1,2 by A3, MATRIX_2:6;
A72: (SpStSeq D) /. 2 = (GoB (SpStSeq D)) * 2,2 by A4, A70, MATRIX_2:6;
A73: (SpStSeq D) /. 3 = (GoB (SpStSeq D)) * 2,1 by A5, A70, MATRIX_2:6;
A74: (SpStSeq D) /. 4 = (GoB (SpStSeq D)) * 1,1 by A6, A70, MATRIX_2:6;
thus SpStSeq D is standard :: thesis:

proof

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

proof

let k be Element of NAT ; :: thesis:
assume k in dom (SpStSeq D) ; :: thesis:
then A75: ( k >= 1 & k <= 5 ) by A2, FINSEQ_3:27;

per cases by A75, NAT_1:30;

suppose A76: k = 1 ; :: thesis:

take 1 ; :: thesis:
take 2 ; :: thesis:
thus [1,2] in Indices (GoB (SpStSeq D)) by A70, MATRIX_2:4; :: thesis:
thus (SpStSeq D) /. k = (GoB (SpStSeq D)) * 1,2 by A3, A70, A76, MATRIX_2:6; :: thesis:

end;

suppose A77: k = 2 ; :: thesis:

take 2 ; :: thesis:
take 2 ; :: thesis:
thus [2,2] in Indices (GoB (SpStSeq D)) by A70, MATRIX_2:4; :: thesis:
thus (SpStSeq D) /. k = (GoB (SpStSeq D)) * 2,2 by A4, A70, A77, MATRIX_2:6; :: thesis:

end;

suppose A78: k = 3 ; :: thesis:

take 2 ; :: thesis:
take 1 ; :: thesis:
thus [2,1] in Indices (GoB (SpStSeq D)) by A70, MATRIX_2:4; :: thesis:
thus (SpStSeq D) /. k = (GoB (SpStSeq D)) * 2,1 by A5, A70, A78, MATRIX_2:6; :: thesis:

end;

suppose A79: k = 4 ; :: thesis:

take 1 ; :: thesis:
take 1 ; :: thesis:
thus [1,1] in Indices (GoB (SpStSeq D)) by A70, MATRIX_2:4; :: thesis:
thus (SpStSeq D) /. k = (GoB (SpStSeq D)) * 1,1 by A6, A70, A79, MATRIX_2:6; :: thesis:

end;

suppose A80: k = 5 ; :: thesis:

end;

let n be Element of NAT ; :: thesis:
assume that
A81: n in dom (SpStSeq D) and
A82: n + 1 in dom (SpStSeq D) ; :: thesis:
let m, k, i, j be Element of NAT ; :: thesis:
assume that
A83: [m,k] in Indices (GoB (SpStSeq D)) and
A84: [i,j] in Indices (GoB (SpStSeq D)) and
A85: (SpStSeq D) /. n = (GoB (SpStSeq D)) * m,k and
A86: (SpStSeq D) /. (n + 1) = (GoB (SpStSeq D)) * i,j ; :: thesis:
A87: n <> 0 by A81, FINSEQ_3:27;
n + 1 <= 4 + 1 by A2, A82, FINSEQ_3:27;
then A88: n <= 4 by XREAL_1:8;

per cases by A87, A88, NAT_1:29;

suppose A89: n = 1 ; :: thesis:

[1,2] in Indices (GoB (SpStSeq D)) by A70, MATRIX_2:4;
then A90: ( m = 1 & k = 2 ) by A71, A83, A85, A89, GOBOARD1:21;
[2,2] in Indices (GoB (SpStSeq D)) by A70, MATRIX_2:4;
then A91: ( i = 1 + 1 & j = 2 ) by A72, A84, A86, A89, GOBOARD1:21;
then abs (m - i) = 1 by A90, GOBOARD1:1;
hence (abs (m - i)) + (abs (k - j)) = 1 by A90, A91, GOBOARD1:2; :: thesis:

end;

suppose A92: n = 2 ; :: thesis:

[2,2] in Indices (GoB (SpStSeq D)) by A70, MATRIX_2:4;
then A93: ( m = 2 & k = 1 + 1 ) by A72, A83, A85, A92, GOBOARD1:21;
[2,1] in Indices (GoB (SpStSeq D)) by A70, MATRIX_2:4;
then A94: ( i = 2 & j = 1 ) by A73, A84, A86, A92, GOBOARD1:21;
then abs (k - j) = 1 by A93, GOBOARD1:1;
hence (abs (m - i)) + (abs (k - j)) = 1 by A93, A94, GOBOARD1:2; :: thesis:

end;

suppose A95: n = 3 ; :: thesis:

[2,1] in Indices (GoB (SpStSeq D)) by A70, MATRIX_2:4;
then A96: ( m = 1 + 1 & k = 1 ) by A73, A83, A85, A95, GOBOARD1:21;
[1,1] in Indices (GoB (SpStSeq D)) by A70, MATRIX_2:4;
then A97: ( i = 1 & j = 1 ) by A74, A84, A86, A95, GOBOARD1:21;
then abs (m - i) = 1 by A96, GOBOARD1:1;
hence (abs (m - i)) + (abs (k - j)) = 1 by A96, A97, GOBOARD1:2; :: thesis:

end;

suppose A98: n = 4 ; :: thesis:

[1,1] in Indices (GoB (SpStSeq D)) by A70, MATRIX_2:4;
then A99: ( m = 1 & k = 1 ) by A74, A83, A85, A98, GOBOARD1:21;
[1,2] in Indices (GoB (SpStSeq D)) by A70, MATRIX_2:4;
then A100: ( i = 1 & j = 1 + 1 ) by A3, A7, A71, A84, A86, A98, GOBOARD1:21;
then abs (k - j) = 1 by A99, GOBOARD1:1;
hence (abs (m - i)) + (abs (k - j)) = 1 by A99, A100, GOBOARD1:2; :: thesis:

end;