A1: <*(S-bound D),(N-bound D)*> is increasing

proof

let n, m be Element of NAT ; :: according to SEQM_3:def 1 :: thesis: ( not n in K1(<*(S-bound D),(N-bound D)*>) or not m in K1(<*(S-bound D),(N-bound D)*>) or m <= n or not K512(<*(S-bound D),(N-bound D)*>,m) <= K512(<*(S-bound D),(N-bound D)*>,n) )
assume that
A2: n in dom <*(S-bound D),(N-bound D)*> and
A3: m in dom <*(S-bound D),(N-bound D)*> ; :: thesis: ( m <= n or not K512(<*(S-bound D),(N-bound D)*>,m) <= K512(<*(S-bound D),(N-bound D)*>,n) )
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: not K512(<*(S-bound D),(N-bound D)*>,m) <= K512(<*(S-bound D),(N-bound D)*>,n)
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 <*(S-bound D),(N-bound D)*> . n < <*(S-bound D),(N-bound D)*> . m by A8, Th34; :: thesis: verum

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 = <*(N-bound D),(N-bound D),(S-bound D)*>;
set Yf2 = <*(S-bound D),(N-bound D)*>;
set Xf1 = <*(W-bound D),(E-bound D),(E-bound D)*>;
set Xf2 = <*(W-bound D),(W-bound D)*>;
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 = <*(W-bound D),(E-bound D),(E-bound D)*> ^ <*(W-bound D),(W-bound D)*> as FinSequence of REAL ;
A9: rng <*(W-bound D),(W-bound D)*> = {(W-bound D),(W-bound D)} by FINSEQ_2:127
.= {(W-bound D)} by ENUMSET1:29 ;
rng <*(W-bound D),(E-bound D),(E-bound D)*> = {(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: <*(W-bound D),(E-bound D)*> is increasing

proof

let n, m be Element of NAT ; :: according to SEQM_3:def 1 :: thesis: ( not n in K1(<*(W-bound D),(E-bound D)*>) or not m in K1(<*(W-bound D),(E-bound D)*>) or m <= n or not K512(<*(W-bound D),(E-bound D)*>,m) <= K512(<*(W-bound D),(E-bound D)*>,n) )
assume that
A13: n in dom <*(W-bound D),(E-bound D)*> and
A14: m in dom <*(W-bound D),(E-bound D)*> ; :: thesis: ( m <= n or not K512(<*(W-bound D),(E-bound D)*>,m) <= K512(<*(W-bound D),(E-bound D)*>,n) )
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: not K512(<*(W-bound D),(E-bound D)*>,m) <= K512(<*(W-bound D),(E-bound D)*>,n)
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 <*(W-bound D),(E-bound D)*> . n < <*(W-bound D),(E-bound D)*> . m by A19, Th33; :: thesis: verum

end;

A20: 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 ;
A21: rng <*(S-bound D),(N-bound D)*> = {(S-bound D),(N-bound D)} by FINSEQ_2:127;
rng <*(N-bound D),(N-bound D),(S-bound D)*> = {(N-bound D),(N-bound D),(S-bound D)} by FINSEQ_2:128
.= {(S-bound D),(N-bound D)} by ENUMSET1:30 ;
then A22: rng Yf = {(S-bound D),(N-bound D)} \/ {(S-bound D),(N-bound D)} by A21, FINSEQ_1:31
.= {(S-bound D),(N-bound D)} ;
then A23: rng <*(S-bound D),(N-bound D)*> = rng Yf by FINSEQ_2:127;
A24: len <*(S-bound D),(N-bound D)*> = 2 by FINSEQ_1:44
.= card (rng Yf) by A20, A22, CARD_2:57 ;
A25: len <*(N-bound D),(N-bound D),(S-bound D)*> = 3 by FINSEQ_1:45;
then 1 in dom <*(N-bound D),(N-bound D),(S-bound D)*> by FINSEQ_3:25;
then A26: Yf . 1 = <*(N-bound D),(N-bound D),(S-bound D)*> . 1 by FINSEQ_1:def 7
.= N-bound D by FINSEQ_1:45 ;
A27: len <*(S-bound D),(N-bound D)*> = 2 by FINSEQ_1:44;
then A28: len Yf = 3 + 2 by A25, FINSEQ_1:22;
2 in dom <*(S-bound D),(N-bound D)*> by A27, FINSEQ_3:25;
then A29: Yf . (3 + 2) = <*(S-bound D),(N-bound D)*> . 2 by A25, FINSEQ_1:def 7
.= N-bound D by FINSEQ_1:44 ;
3 in dom <*(N-bound D),(N-bound D),(S-bound D)*> by A25, FINSEQ_3:25;
then A30: Yf . 3 = <*(N-bound D),(N-bound D),(S-bound D)*> . 3 by FINSEQ_1:def 7
.= S-bound D by FINSEQ_1:45 ;
2 in dom <*(N-bound D),(N-bound D),(S-bound D)*> by A25, FINSEQ_3:25;
then A31: Yf . 2 = <*(N-bound D),(N-bound D),(S-bound D)*> . 2 by FINSEQ_1:def 7
.= N-bound D by FINSEQ_1:45 ;
A32: len <*(NW-corner D),(NE-corner D),(SE-corner D)*> = 3 by FINSEQ_1:45;
then 1 in dom <*(NW-corner D),(NE-corner D),(SE-corner D)*> by FINSEQ_3:25;
then A33: (SpStSeq D) /. 1 = <*(NW-corner D),(NE-corner D),(SE-corner D)*> /. 1 by FINSEQ_4:68
.= NW-corner D by FINSEQ_4:18 ;
3 in dom <*(NW-corner D),(NE-corner D),(SE-corner D)*> by A32, FINSEQ_3:25;
then A34: (SpStSeq D) /. 3 = <*(NW-corner D),(NE-corner D),(SE-corner D)*> /. 3 by FINSEQ_4:68
.= SE-corner D by FINSEQ_4:18 ;
2 in dom <*(NW-corner D),(NE-corner D),(SE-corner D)*> by A32, FINSEQ_3:25;
then A35: (SpStSeq D) /. 2 = <*(NW-corner D),(NE-corner D),(SE-corner D)*> /. 2 by FINSEQ_4:68
.= NE-corner D by FINSEQ_4:18 ;
A36: len <*(SW-corner D),(NW-corner D)*> = 2 by FINSEQ_1:44;
then A37: len (<*(NW-corner D),(NE-corner D),(SE-corner D)*> ^ <*(SW-corner D),(NW-corner D)*>) = 3 + 2 by A32, FINSEQ_1:22;
1 in dom <*(SW-corner D),(NW-corner D)*> by A36, FINSEQ_3:25;
then A38: (SpStSeq D) /. (3 + 1) = <*(SW-corner D),(NW-corner D)*> /. 1 by A32, FINSEQ_4:69
.= SW-corner D by FINSEQ_4:17 ;
then A39: LSeg ((SpStSeq D),3) = LSeg ((SE-corner D),(SW-corner D)) by A37, A34, TOPREAL1:def 3;
2 in dom <*(SW-corner D),(NW-corner D)*> by A36, FINSEQ_3:25;
then A40: (SpStSeq D) /. (3 + 2) = <*(SW-corner D),(NW-corner D)*> /. 2 by A32, FINSEQ_4:69
.= NW-corner D by FINSEQ_4:17 ;
thus SpStSeq D is special :: thesis: ( SpStSeq D is unfolded & SpStSeq D is circular & SpStSeq D is s.c.c. & SpStSeq D is standard )

proof

let i be Nat; :: according to TOPREAL1:def 5 :: thesis: ( not 1 <= i or not i + 1 <= len (SpStSeq D) or ((SpStSeq D) /. i) `1 = ((SpStSeq D) /. (i + 1)) `1 or ((SpStSeq D) /. i) `2 = ((SpStSeq D) /. (i + 1)) `2 )
assume 1 <= i ; :: thesis: ( not i + 1 <= len (SpStSeq D) or ((SpStSeq D) /. i) `1 = ((SpStSeq D) /. (i + 1)) `1 or ((SpStSeq D) /. i) `2 = ((SpStSeq D) /. (i + 1)) `2 )
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: ( ((SpStSeq D) /. i) `1 = ((SpStSeq D) /. (i + 1)) `1 or ((SpStSeq D) /. i) `2 = ((SpStSeq D) /. (i + 1)) `2 )
then A42: ( i + 1 = 1 + 1 or i + 1 = 2 + 1 or i + 1 = 3 + 1 or i + 1 = 4 + 1 ) by A37, A41, NAT_1:29;

per cases ( i = 1 or i = 2 or i = 3 or i = 4 ) by A42;

suppose A43: i = 1 ; :: thesis: ( ((SpStSeq D) /. i) `1 = ((SpStSeq D) /. (i + 1)) `1 or ((SpStSeq D) /. i) `2 = ((SpStSeq D) /. (i + 1)) `2 )

((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: verum

end;

suppose A44: i = 2 ; :: thesis: ( ((SpStSeq D) /. i) `1 = ((SpStSeq D) /. (i + 1)) `1 or ((SpStSeq D) /. i) `2 = ((SpStSeq D) /. (i + 1)) `2 )

((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: verum

end;

suppose A45: i = 3 ; :: thesis: ( ((SpStSeq D) /. i) `1 = ((SpStSeq D) /. (i + 1)) `1 or ((SpStSeq D) /. i) `2 = ((SpStSeq D) /. (i + 1)) `2 )

((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: verum

end;

suppose A46: i = 4 ; :: thesis: ( ((SpStSeq D) /. i) `1 = ((SpStSeq D) /. (i + 1)) `1 or ((SpStSeq D) /. i) `2 = ((SpStSeq D) /. (i + 1)) `2 )

((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: verum

end;

end;

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 <*(S-bound D),(N-bound D)*> by A27, FINSEQ_3:25;
then A49: Yf . (3 + 1) = <*(S-bound D),(N-bound D)*> . 1 by A25, FINSEQ_1:def 7
.= S-bound D by FINSEQ_1:44 ;

now

let n be Element of NAT ; :: thesis: ( n in dom Yf implies Yf . b₁ = ((SpStSeq D) /. b₁) `2 )
assume A50: n in dom Yf ; :: thesis: Yf . b<sub>1</sub> = ((SpStSeq D) /. b<sub>1</sub>) `2
then A51: n <> 0 by FINSEQ_3:25;
A52: n <= 5 by A28, A50, FINSEQ_3:25;

per cases ( n = 1 or n = 2 or n = 3 or n = 4 or n = 5 ) by A51, A52, NAT_1:29;

suppose n = 1 ; :: thesis: Yf . b₁ = ((SpStSeq D) /. b₁) `2

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

end;

suppose n = 2 ; :: thesis: Yf . b₁ = ((SpStSeq D) /. b₁) `2

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

end;

suppose n = 3 ; :: thesis: Yf . b₁ = ((SpStSeq D) /. b₁) `2

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

end;

suppose n = 4 ; :: thesis: Yf . b₁ = ((SpStSeq D) /. b₁) `2

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

end;

suppose n = 5 ; :: thesis: Yf . b₁ = ((SpStSeq D) /. b₁) `2

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

end;

end;

end;

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

proof

let i be Nat; :: according to TOPREAL1:def 6 :: thesis: ( not 1 <= i or not i + 2 <= len (SpStSeq D) or (LSeg ((SpStSeq D),i)) /\ (LSeg ((SpStSeq D),(i + 1))) = {((SpStSeq D) /. (i + 1))} )
assume 1 <= i ; :: thesis: ( not i + 2 <= len (SpStSeq D) or (LSeg ((SpStSeq D),i)) /\ (LSeg ((SpStSeq D),(i + 1))) = {((SpStSeq D) /. (i + 1))} )
then A55: 1 + 2 <= i + 2 by XREAL_1:6;
then A56: 1 < i + 2 by XXREAL_0:2;
assume A57: i + 2 <= len (SpStSeq D) ; :: thesis: (LSeg ((SpStSeq D),i)) /\ (LSeg ((SpStSeq D),(i + 1))) = {((SpStSeq D) /. (i + 1))}
2 < i + 2 by A55, XXREAL_0:2;
then A58: ( i + 2 = 1 + 2 or i + 2 = 2 + 2 or i + 2 = 3 + 2 ) by A37, A56, A57, NAT_1:29;

per cases ( i = 1 or i = 2 or i = 3 ) by A58;

suppose i = 1 ; :: thesis: (LSeg ((SpStSeq D),i)) /\ (LSeg ((SpStSeq D),(i + 1))) = {((SpStSeq D) /. (i + 1))}

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

end;

suppose i = 2 ; :: thesis: (LSeg ((SpStSeq D),i)) /\ (LSeg ((SpStSeq D),(i + 1))) = {((SpStSeq D) /. (i + 1))}

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

end;

suppose i = 3 ; :: thesis: (LSeg ((SpStSeq D),i)) /\ (LSeg ((SpStSeq D),(i + 1))) = {((SpStSeq D) /. (i + 1))}

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

end;

end;

end;

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

proof

let i be Element of NAT ; :: according to GOBOARD5:def 4 :: thesis: for b₁ being Element of NAT holds
( b₁ <= i + 1 or ( ( i <= 1 or len (SpStSeq D) <= b₁ ) & len (SpStSeq D) <= b₁ + 1 ) or LSeg ((SpStSeq D),i) misses LSeg ((SpStSeq D),b₁) )
let j be Element of NAT ; :: thesis: ( j <= i + 1 or ( ( i <= 1 or len (SpStSeq D) <= j ) & len (SpStSeq D) <= j + 1 ) or LSeg ((SpStSeq D),i) misses LSeg ((SpStSeq D),j) )
assume that
A59: i + 1 < j and
A60: ( ( i > 1 & j < len (SpStSeq D) ) or j + 1 < len (SpStSeq D) ) ; :: thesis: LSeg ((SpStSeq D),i) misses LSeg ((SpStSeq D),j)
A61: ( 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 A37, A60, NAT_1:29;
A62: ( i + 2 = 2 + 2 implies i = 2 ) ;
A63: ( i + 2 = 1 + 2 implies i = 1 ) ;
A64: (i + 1) + 1 = i + (1 + 1) ;
then A65: i + 2 <> 0 + 1 ;
A66: ( i + 2 = 0 + 2 implies i = 0 ) ;
A67: i + 2 <= j by A59, A64, NAT_1:13;

A68: now

per cases ( j = 2 or j = 3 or j = 4 ) by A59, A61, NAT_1:11;

case j = 2 ; :: thesis: i = 0

hence i = 0 by A59, A64, A66, NAT_1:26; :: thesis: verum

end;

case j = 3 ; :: thesis: ( i = 0 or i = 1 )

hence ( i = 0 or i = 1 ) by A59, A64, A63, A66, NAT_1:27; :: thesis: verum

end;

case j = 4 ; :: thesis: ( i = 0 or i = 2 )

hence ( i = 0 or i = 2 ) by A37, A60, A67, A62, A63, A66, A65, NAT_1:28; :: thesis: verum

end;

end;

end;

per cases ( i = 0 or ( i = 1 & j = 3 ) or ( i = 2 & j = 4 ) ) by A68;

suppose i = 0 ; :: thesis: LSeg ((SpStSeq D),i) misses LSeg ((SpStSeq D),j)

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: verum

end;

suppose ( i = 1 & j = 3 ) ; :: thesis: LSeg ((SpStSeq D),i) misses LSeg ((SpStSeq D),j)

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

end;

suppose ( i = 2 & j = 4 ) ; :: thesis: LSeg ((SpStSeq D),i) misses LSeg ((SpStSeq D),j)

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

end;

end;

end;

A69: W-bound D < E-bound D by Th33;
A70: len <*(W-bound D),(E-bound D)*> = 2 by FINSEQ_1:44
.= card (rng Xf) by A69, A10, CARD_2:57 ;
A71: len <*(W-bound D),(E-bound D),(E-bound D)*> = 3 by FINSEQ_1:45;
then 1 in dom <*(W-bound D),(E-bound D),(E-bound D)*> by FINSEQ_3:25;
then A72: Xf . 1 = <*(W-bound D),(E-bound D),(E-bound D)*> . 1 by FINSEQ_1:def 7
.= W-bound D by FINSEQ_1:45 ;
A73: len <*(W-bound D),(W-bound D)*> = 2 by FINSEQ_1:44;
then A74: len Xf = 3 + 2 by A71, FINSEQ_1:22;
2 in dom <*(W-bound D),(W-bound D)*> by A73, FINSEQ_3:25;
then A75: Xf . (3 + 2) = <*(W-bound D),(W-bound D)*> . 2 by A71, FINSEQ_1:def 7
.= W-bound D by FINSEQ_1:44 ;
3 in dom <*(W-bound D),(E-bound D),(E-bound D)*> by A71, FINSEQ_3:25;
then A76: Xf . 3 = <*(W-bound D),(E-bound D),(E-bound D)*> . 3 by FINSEQ_1:def 7
.= E-bound D by FINSEQ_1:45 ;
2 in dom <*(W-bound D),(E-bound D),(E-bound D)*> by A71, FINSEQ_3:25;
then A77: Xf . 2 = <*(W-bound D),(E-bound D),(E-bound D)*> . 2 by FINSEQ_1:def 7
.= E-bound D by FINSEQ_1:45 ;
1 in dom <*(W-bound D),(W-bound D)*> by A73, FINSEQ_3:25;
then A78: Xf . (3 + 1) = <*(W-bound D),(W-bound D)*> . 1 by A71, FINSEQ_1:def 7
.= W-bound D by FINSEQ_1:44 ;

now

let n be Element of NAT ; :: thesis: ( n in dom Xf implies Xf . b₁ = ((SpStSeq D) /. b₁) `1 )
assume A79: n in dom Xf ; :: thesis: Xf . b<sub>1</sub> = ((SpStSeq D) /. b<sub>1</sub>) `1
then A80: n <> 0 by FINSEQ_3:25;
A81: n <= 5 by A74, A79, FINSEQ_3:25;

per cases ( n = 1 or n = 2 or n = 3 or n = 4 or n = 5 ) by A80, A81, NAT_1:29;

suppose n = 1 ; :: thesis: Xf . b₁ = ((SpStSeq D) /. b₁) `1

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

end;

suppose n = 2 ; :: thesis: Xf . b₁ = ((SpStSeq D) /. b₁) `1

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

end;

suppose n = 3 ; :: thesis: Xf . b₁ = ((SpStSeq D) /. b₁) `1

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

end;

suppose n = 4 ; :: thesis: Xf . b₁ = ((SpStSeq D) /. b₁) `1

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

end;

suppose n = 5 ; :: thesis: Xf . b₁ = ((SpStSeq D) /. b₁) `1

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

end;

end;

end;

then Xf = X_axis (SpStSeq D) by A37, A74, GOBOARD1:def 1;
then A82: <*(W-bound D),(E-bound D)*> = Incr (X_axis (SpStSeq D)) by A11, A70, A12, SEQ_4:def 21;
A83: for n, m being Element of NAT st [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)]|)) holds
((|[(W-bound D),(S-bound D)]|,|[(W-bound D),(N-bound D)]|) ][ (|[(E-bound D),(S-bound D)]|,|[(E-bound D),(N-bound D)]|)) * (n,m) = |[((Incr (X_axis (SpStSeq D))) . n),((Incr (Y_axis (SpStSeq D))) . m)]|

proof

let n, m be Element of NAT ; :: thesis: ( [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)]|)) implies ((|[(W-bound D),(S-bound D)]|,|[(W-bound D),(N-bound D)]|) ][ (|[(E-bound D),(S-bound D)]|,|[(E-bound D),(N-bound D)]|)) * (n,m) = |[((Incr (X_axis (SpStSeq D))) . n),((Incr (Y_axis (SpStSeq D))) . m)]| )
A84: <*(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: ((|[(W-bound D),(S-bound D)]|,|[(W-bound D),(N-bound D)]|) ][ (|[(E-bound D),(S-bound D)]|,|[(E-bound D),(N-bound D)]|)) * (n,m) = |[((Incr (X_axis (SpStSeq D))) . n),((Incr (Y_axis (SpStSeq D))) . m)]|
then [n,m] in [:{1,2},{1,2}:] by FINSEQ_1:2, MATRIX_2:3;
then A85: [n,m] in {[1,1],[1,2],[2,1],[2,2]} by MCART_1:23;
A86: <*(S-bound D),(N-bound D)*> . 2 = N-bound D by FINSEQ_1:44;

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

suppose A87: [n,m] = [1,1] ; :: thesis: ((|[(W-bound D),(S-bound D)]|,|[(W-bound D),(N-bound D)]|) ][ (|[(E-bound D),(S-bound D)]|,|[(E-bound D),(N-bound D)]|)) * (n,m) = |[((Incr (X_axis (SpStSeq D))) . n),((Incr (Y_axis (SpStSeq D))) . m)]|

then A88: m = 1 by ZFMISC_1:27;
A89: n = 1 by A87, ZFMISC_1:27;
hence ((|[(W-bound D),(S-bound D)]|,|[(W-bound D),(N-bound D)]|) ][ (|[(E-bound D),(S-bound D)]|,|[(E-bound D),(N-bound D)]|)) * (n,m) = |[(W-bound D),(S-bound D)]| by A88, MATRIX_2:6
.= |[((Incr (X_axis (SpStSeq D))) . n),((Incr (Y_axis (SpStSeq D))) . m)]| by A82, A53, A84, A89, A88, FINSEQ_1:44 ;
:: thesis: verum

end;

suppose A90: [n,m] = [1,2] ; :: thesis: ((|[(W-bound D),(S-bound D)]|,|[(W-bound D),(N-bound D)]|) ][ (|[(E-bound D),(S-bound D)]|,|[(E-bound D),(N-bound D)]|)) * (n,m) = |[((Incr (X_axis (SpStSeq D))) . n),((Incr (Y_axis (SpStSeq D))) . m)]|

then A91: m = 2 by ZFMISC_1:27;
A92: n = 1 by A90, ZFMISC_1:27;
hence ((|[(W-bound D),(S-bound D)]|,|[(W-bound D),(N-bound D)]|) ][ (|[(E-bound D),(S-bound D)]|,|[(E-bound D),(N-bound D)]|)) * (n,m) = |[(W-bound D),(N-bound D)]| by A91, MATRIX_2:6
.= |[((Incr (X_axis (SpStSeq D))) . n),((Incr (Y_axis (SpStSeq D))) . m)]| by A82, A53, A86, A92, A91, FINSEQ_1:44 ;
:: thesis: verum

end;

suppose A93: [n,m] = [2,1] ; :: thesis: ((|[(W-bound D),(S-bound D)]|,|[(W-bound D),(N-bound D)]|) ][ (|[(E-bound D),(S-bound D)]|,|[(E-bound D),(N-bound D)]|)) * (n,m) = |[((Incr (X_axis (SpStSeq D))) . n),((Incr (Y_axis (SpStSeq D))) . m)]|

then A94: m = 1 by ZFMISC_1:27;
A95: n = 2 by A93, ZFMISC_1:27;
hence ((|[(W-bound D),(S-bound D)]|,|[(W-bound D),(N-bound D)]|) ][ (|[(E-bound D),(S-bound D)]|,|[(E-bound D),(N-bound D)]|)) * (n,m) = |[(E-bound D),(S-bound D)]| by A94, MATRIX_2:6
.= |[((Incr (X_axis (SpStSeq D))) . n),((Incr (Y_axis (SpStSeq D))) . m)]| by A82, A53, A84, A95, A94, FINSEQ_1:44 ;
:: thesis: verum

end;

suppose A96: [n,m] = [2,2] ; :: thesis: ((|[(W-bound D),(S-bound D)]|,|[(W-bound D),(N-bound D)]|) ][ (|[(E-bound D),(S-bound D)]|,|[(E-bound D),(N-bound D)]|)) * (n,m) = |[((Incr (X_axis (SpStSeq D))) . n),((Incr (Y_axis (SpStSeq D))) . m)]|

then A97: m = 2 by ZFMISC_1:27;
A98: n = 2 by A96, ZFMISC_1:27;
hence ((|[(W-bound D),(S-bound D)]|,|[(W-bound D),(N-bound D)]|) ][ (|[(E-bound D),(S-bound D)]|,|[(E-bound D),(N-bound D)]|)) * (n,m) = |[(E-bound D),(N-bound D)]| by A97, MATRIX_2:6
.= |[((Incr (X_axis (SpStSeq D))) . n),((Incr (Y_axis (SpStSeq D))) . m)]| by A82, A53, A86, A98, A97, FINSEQ_1:44 ;
:: thesis: verum

end;

end;

end;

A99: width ((|[(W-bound D),(S-bound D)]|,|[(W-bound D),(N-bound D)]|) ][ (|[(E-bound D),(S-bound D)]|,|[(E-bound D),(N-bound D)]|)) = 2 by MATRIX_2:3
.= len (Incr (Y_axis (SpStSeq D))) by A53, FINSEQ_1:44 ;
len ((|[(W-bound D),(S-bound D)]|,|[(W-bound D),(N-bound D)]|) ][ (|[(E-bound D),(S-bound D)]|,|[(E-bound D),(N-bound D)]|)) = 2 by MATRIX_2:3
.= len (Incr (X_axis (SpStSeq D))) by A82, FINSEQ_1:44 ;
then A100: (|[(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 A99, A83, GOBOARD2:def 1
.= GoB (SpStSeq D) by GOBOARD2:def 2 ;
then A101: (SpStSeq D) /. 2 = (GoB (SpStSeq D)) * (2,2) by A35, MATRIX_2:6;
A102: (SpStSeq D) /. 4 = (GoB (SpStSeq D)) * (1,1) by A38, A100, MATRIX_2:6;
A103: (SpStSeq D) /. 3 = (GoB (SpStSeq D)) * (2,1) by A34, A100, MATRIX_2:6;
A104: (SpStSeq D) /. 1 = (GoB (SpStSeq D)) * (1,2) by A33, A100, MATRIX_2:6;
thus SpStSeq D is standard :: thesis: verum

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 9,GOBOARD5:def 5 :: thesis: for b₁ being Element of NAT holds
( not b₁ in dom (SpStSeq D) or not b₁ + 1 in dom (SpStSeq D) or for b₂, b₃, b₄, b₅ being Element of NAT holds
( not [b₂,b₃] in Indices (GoB (SpStSeq D)) or not [b₄,b₅] in Indices (GoB (SpStSeq D)) or not (SpStSeq D) /. b₁ = (GoB (SpStSeq D)) * (b₂,b₃) or not (SpStSeq D) /. (b₁ + 1) = (GoB (SpStSeq D)) * (b₄,b₅) or (abs (b₂ - b₄)) + (abs (b₃ - b₅)) = 1 ) )

proof

let k be Element of NAT ; :: thesis: ( k in dom (SpStSeq D) implies ex i, j being Element of NAT st
( [i,j] in Indices (GoB (SpStSeq D)) & (SpStSeq D) /. k = (GoB (SpStSeq D)) * (i,j) ) )
assume A105: k in dom (SpStSeq D) ; :: thesis: ex i, j being Element of NAT st
( [i,j] in Indices (GoB (SpStSeq D)) & (SpStSeq D) /. k = (GoB (SpStSeq D)) * (i,j) )
then A106: k >= 1 by FINSEQ_3:25;
A107: k <= 5 by A37, A105, FINSEQ_3:25;

per cases ( k = 1 or k = 2 or k = 3 or k = 4 or k = 5 ) by A106, A107, NAT_1:29;

suppose A108: k = 1 ; :: thesis: ex i, j being Element of NAT st
( [i,j] in Indices (GoB (SpStSeq D)) & (SpStSeq D) /. k = (GoB (SpStSeq D)) * (i,j) )

take 1 ; :: thesis: ex j being Element of NAT st
( [1,j] in Indices (GoB (SpStSeq D)) & (SpStSeq D) /. k = (GoB (SpStSeq D)) * (1,j) )
take 2 ; :: thesis: ( [1,2] in Indices (GoB (SpStSeq D)) & (SpStSeq D) /. k = (GoB (SpStSeq D)) * (1,2) )
thus [1,2] in Indices (GoB (SpStSeq D)) by A100, MATRIX_2:4; :: thesis: (SpStSeq D) /. k = (GoB (SpStSeq D)) * (1,2)
thus (SpStSeq D) /. k = (GoB (SpStSeq D)) * (1,2) by A33, A100, A108, MATRIX_2:6; :: thesis: verum

end;

suppose A109: k = 2 ; :: thesis: ex i, j being Element of NAT st
( [i,j] in Indices (GoB (SpStSeq D)) & (SpStSeq D) /. k = (GoB (SpStSeq D)) * (i,j) )

take 2 ; :: thesis: ex j being Element of NAT st
( [2,j] in Indices (GoB (SpStSeq D)) & (SpStSeq D) /. k = (GoB (SpStSeq D)) * (2,j) )
take 2 ; :: thesis: ( [2,2] in Indices (GoB (SpStSeq D)) & (SpStSeq D) /. k = (GoB (SpStSeq D)) * (2,2) )
thus [2,2] in Indices (GoB (SpStSeq D)) by A100, MATRIX_2:4; :: thesis: (SpStSeq D) /. k = (GoB (SpStSeq D)) * (2,2)
thus (SpStSeq D) /. k = (GoB (SpStSeq D)) * (2,2) by A35, A100, A109, MATRIX_2:6; :: thesis: verum

end;

suppose A110: k = 3 ; :: thesis: ex i, j being Element of NAT st
( [i,j] in Indices (GoB (SpStSeq D)) & (SpStSeq D) /. k = (GoB (SpStSeq D)) * (i,j) )

take 2 ; :: thesis: ex j being Element of NAT st
( [2,j] in Indices (GoB (SpStSeq D)) & (SpStSeq D) /. k = (GoB (SpStSeq D)) * (2,j) )
take 1 ; :: thesis: ( [2,1] in Indices (GoB (SpStSeq D)) & (SpStSeq D) /. k = (GoB (SpStSeq D)) * (2,1) )
thus [2,1] in Indices (GoB (SpStSeq D)) by A100, MATRIX_2:4; :: thesis: (SpStSeq D) /. k = (GoB (SpStSeq D)) * (2,1)
thus (SpStSeq D) /. k = (GoB (SpStSeq D)) * (2,1) by A34, A100, A110, MATRIX_2:6; :: thesis: verum

end;

suppose A111: k = 4 ; :: thesis: ex i, j being Element of NAT st
( [i,j] in Indices (GoB (SpStSeq D)) & (SpStSeq D) /. k = (GoB (SpStSeq D)) * (i,j) )

take 1 ; :: thesis: ex j being Element of NAT st
( [1,j] in Indices (GoB (SpStSeq D)) & (SpStSeq D) /. k = (GoB (SpStSeq D)) * (1,j) )
take 1 ; :: thesis: ( [1,1] in Indices (GoB (SpStSeq D)) & (SpStSeq D) /. k = (GoB (SpStSeq D)) * (1,1) )
thus [1,1] in Indices (GoB (SpStSeq D)) by A100, MATRIX_2:4; :: thesis: (SpStSeq D) /. k = (GoB (SpStSeq D)) * (1,1)
thus (SpStSeq D) /. k = (GoB (SpStSeq D)) * (1,1) by A38, A100, A111, MATRIX_2:6; :: thesis: verum

end;

suppose A112: k = 5 ; :: thesis: ex i, j being Element of NAT st
( [i,j] in Indices (GoB (SpStSeq D)) & (SpStSeq D) /. k = (GoB (SpStSeq D)) * (i,j) )

take 1 ; :: thesis: ex j being Element of NAT st
( [1,j] in Indices (GoB (SpStSeq D)) & (SpStSeq D) /. k = (GoB (SpStSeq D)) * (1,j) )
take 2 ; :: thesis: ( [1,2] in Indices (GoB (SpStSeq D)) & (SpStSeq D) /. k = (GoB (SpStSeq D)) * (1,2) )
thus [1,2] in Indices (GoB (SpStSeq D)) by A100, MATRIX_2:4; :: thesis: (SpStSeq D) /. k = (GoB (SpStSeq D)) * (1,2)
thus (SpStSeq D) /. k = (GoB (SpStSeq D)) * (1,2) by A40, A100, A112, MATRIX_2:6; :: thesis: verum

end;

end;

end;

let n be Element of NAT ; :: thesis: ( not n in dom (SpStSeq D) or not n + 1 in dom (SpStSeq D) or for b₁, b₂, b₃, b₄ being Element of NAT holds
( not [b₁,b₂] in Indices (GoB (SpStSeq D)) or not [b₃,b₄] in Indices (GoB (SpStSeq D)) or not (SpStSeq D) /. n = (GoB (SpStSeq D)) * (b₁,b₂) or not (SpStSeq D) /. (n + 1) = (GoB (SpStSeq D)) * (b₃,b₄) or (abs (b₁ - b₃)) + (abs (b₂ - b₄)) = 1 ) )
assume that
A113: n in dom (SpStSeq D) and
A114: n + 1 in dom (SpStSeq D) ; :: thesis: for b₁, b₂, b₃, b₄ being Element of NAT holds
( not [b₁,b₂] in Indices (GoB (SpStSeq D)) or not [b₃,b₄] in Indices (GoB (SpStSeq D)) or not (SpStSeq D) /. n = (GoB (SpStSeq D)) * (b₁,b₂) or not (SpStSeq D) /. (n + 1) = (GoB (SpStSeq D)) * (b₃,b₄) or (abs (b₁ - b₃)) + (abs (b₂ - b₄)) = 1 )
A115: n <> 0 by A113, FINSEQ_3:25;
n + 1 <= 4 + 1 by A37, A114, FINSEQ_3:25;
then A116: n <= 4 by XREAL_1:6;
let m, k, i, j be Element of NAT ; :: thesis: ( not [m,k] in Indices (GoB (SpStSeq D)) or not [i,j] in Indices (GoB (SpStSeq D)) or not (SpStSeq D) /. n = (GoB (SpStSeq D)) * (m,k) or not (SpStSeq D) /. (n + 1) = (GoB (SpStSeq D)) * (i,j) or (abs (m - i)) + (abs (k - j)) = 1 )
assume that
A117: [m,k] in Indices (GoB (SpStSeq D)) and
A118: [i,j] in Indices (GoB (SpStSeq D)) and
A119: (SpStSeq D) /. n = (GoB (SpStSeq D)) * (m,k) and
A120: (SpStSeq D) /. (n + 1) = (GoB (SpStSeq D)) * (i,j) ; :: thesis: (abs (m - i)) + (abs (k - j)) = 1

per cases ( n = 1 or n = 2 or n = 3 or n = 4 ) by A115, A116, NAT_1:28;

suppose A121: n = 1 ; :: thesis: (abs (m - i)) + (abs (k - j)) = 1

A122: [2,2] in Indices (GoB (SpStSeq D)) by A100, MATRIX_2:4;
then A123: i = 1 + 1 by A101, A118, A120, A121, GOBOARD1:5;
A124: [1,2] in Indices (GoB (SpStSeq D)) by A100, MATRIX_2:4;
then m = 1 by A104, A117, A119, A121, GOBOARD1:5;
then A125: abs (m - i) = 1 by A123, SEQM_3:41;
A126: j = 2 by A101, A118, A120, A121, A122, GOBOARD1:5;
k = 2 by A104, A117, A119, A121, A124, GOBOARD1:5;
hence (abs (m - i)) + (abs (k - j)) = 1 by A126, A125, SEQM_3:42; :: thesis: verum

end;

suppose A127: n = 2 ; :: thesis: (abs (m - i)) + (abs (k - j)) = 1

A128: [2,1] in Indices (GoB (SpStSeq D)) by A100, MATRIX_2:4;
then A129: j = 1 by A103, A118, A120, A127, GOBOARD1:5;
A130: [2,2] in Indices (GoB (SpStSeq D)) by A100, MATRIX_2:4;
then k = 1 + 1 by A101, A117, A119, A127, GOBOARD1:5;
then A131: abs (k - j) = 1 by A129, SEQM_3:41;
A132: i = 2 by A103, A118, A120, A127, A128, GOBOARD1:5;
m = 2 by A101, A117, A119, A127, A130, GOBOARD1:5;
hence (abs (m - i)) + (abs (k - j)) = 1 by A132, A131, SEQM_3:42; :: thesis: verum

end;

suppose A133: n = 3 ; :: thesis: (abs (m - i)) + (abs (k - j)) = 1

A134: [1,1] in Indices (GoB (SpStSeq D)) by A100, MATRIX_2:4;
then A135: i = 1 by A102, A118, A120, A133, GOBOARD1:5;
A136: [2,1] in Indices (GoB (SpStSeq D)) by A100, MATRIX_2:4;
then m = 1 + 1 by A103, A117, A119, A133, GOBOARD1:5;
then A137: abs (m - i) = 1 by A135, SEQM_3:41;
A138: j = 1 by A102, A118, A120, A133, A134, GOBOARD1:5;
k = 1 by A103, A117, A119, A133, A136, GOBOARD1:5;
hence (abs (m - i)) + (abs (k - j)) = 1 by A138, A137, SEQM_3:42; :: thesis: verum

end;

suppose A139: n = 4 ; :: thesis: (abs (m - i)) + (abs (k - j)) = 1

A140: [1,1] in Indices (GoB (SpStSeq D)) by A100, MATRIX_2:4;
then A141: k = 1 by A102, A117, A119, A139, GOBOARD1:5;
A142: [1,2] in Indices (GoB (SpStSeq D)) by A100, MATRIX_2:4;
then j = 1 + 1 by A33, A40, A104, A118, A120, A139, GOBOARD1:5;
then A143: abs (k - j) = 1 by A141, SEQM_3:41;
A144: m = 1 by A102, A117, A119, A139, A140, GOBOARD1:5;
i = 1 by A33, A40, A104, A118, A120, A139, A142, GOBOARD1:5;
hence (abs (m - i)) + (abs (k - j)) = 1 by A144, A143, SEQM_3:42; :: thesis: verum

end;

end;

end;