set f1 = <*|[0 ,0 ]|,|[0 ,1]|,|[1,1]|*>;
set f2 = <*|[1,0 ]|,|[0 ,0 ]|*>;
A1: ( len <*|[0 ,0 ]|,|[0 ,1]|,|[1,1]|*> = 3 & len <*|[1,0 ]|,|[0 ,0 ]|*> = 2 ) by FINSEQ_1:61, FINSEQ_1:62;
then A2: len (<*|[0 ,0 ]|,|[0 ,1]|,|[1,1]|*> ^ <*|[1,0 ]|,|[0 ,0 ]|*>) = 3 + 2 by FINSEQ_1:35;
then reconsider f = <*|[0 ,0 ]|,|[0 ,1]|,|[1,1]|*> ^ <*|[1,0 ]|,|[0 ,0 ]|*> as non empty FinSequence of (TOP-REAL 2) by CARD_1:47;
take f ; :: thesis:
A3: 1 in dom <*|[0 ,0 ]|,|[0 ,1]|,|[1,1]|*> by A1, FINSEQ_3:27;
then A4: f /. 1 = <*|[0 ,0 ]|,|[0 ,1]|,|[1,1]|*> /. 1 by FINSEQ_4:83
.= |[0 ,0 ]| by FINSEQ_4:27 ;
A5: 2 in dom <*|[0 ,0 ]|,|[0 ,1]|,|[1,1]|*> by A1, FINSEQ_3:27;
then A6: f /. 2 = <*|[0 ,0 ]|,|[0 ,1]|,|[1,1]|*> /. 2 by FINSEQ_4:83
.= |[0 ,1]| by FINSEQ_4:27 ;
A7: dom <*|[0 ,0 ]|,|[0 ,1]|,|[1,1]|*> c= dom f by FINSEQ_1:39;
then ( f . 1 = f /. 1 & f . 2 = f /. 2 ) by A3, A5, PARTFUN1:def 8;
then f . 1 <> f . 2 by A4, A6, SPPOL_2:1;
hence not f is constant by A3, A5, A7, GOBOARD1:def 2; :: thesis:
3 in dom <*|[0 ,0 ]|,|[0 ,1]|,|[1,1]|*> by A1, FINSEQ_3:27;
then A8: f /. 3 = <*|[0 ,0 ]|,|[0 ,1]|,|[1,1]|*> /. 3 by FINSEQ_4:83
.= |[1,1]| by FINSEQ_4:27 ;
1 in dom <*|[1,0 ]|,|[0 ,0 ]|*> by A1, FINSEQ_3:27;
then A9: f /. (3 + 1) = <*|[1,0 ]|,|[0 ,0 ]|*> /. 1 by A1, FINSEQ_4:84
.= |[1,0 ]| by FINSEQ_4:26 ;
2 in dom <*|[1,0 ]|,|[0 ,0 ]|*> by A1, FINSEQ_3:27;
then A10: f /. (3 + 2) = <*|[1,0 ]|,|[0 ,0 ]|*> /. 2 by A1, FINSEQ_4:84
.= |[0 ,0 ]| by FINSEQ_4:26 ;
1 + 1 = 2 ;
then A11: LSeg f,1 = LSeg |[0 ,0 ]|,|[0 ,1]| by A2, A4, A6, TOPREAL1:def 5;
2 + 1 = 3 ;
then A12: LSeg f,2 = LSeg |[0 ,1]|,|[1,1]| by A2, A6, A8, TOPREAL1:def 5;
A13: LSeg f,3 = LSeg |[1,1]|,|[1,0 ]| by A2, A8, A9, TOPREAL1:def 5;
4 + 1 = 5 ;
then A14: LSeg f,4 = LSeg |[1,0 ]|,|[0 ,0 ]| by A2, A9, A10, TOPREAL1:def 5;
thus f 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 A15: ( 1 < i + 1 & 0 < i + 1 ) by XXREAL_0:2;
assume i + 1 <= len f ; :: thesis:
then A16: ( i + 1 = 1 + 1 or i + 1 = 2 + 1 or i + 1 = 3 + 1 or i + 1 = 4 + 1 ) by A2, A15, NAT_1:30;

per cases by A16;

suppose A17: i = 1 ; :: thesis:

(f /. 1) `1 = 0 by A4, EUCLID:56
.= (f /. (1 + 1)) `1 by A6, EUCLID:56 ;
hence ( (f /. i) `1 = (f /. (i + 1)) `1 or (f /. i) `2 = (f /. (i + 1)) `2 ) by A17; :: thesis:

end;

suppose A18: i = 2 ; :: thesis:

(f /. 2) `2 = 1 by A6, EUCLID:56
.= (f /. (2 + 1)) `2 by A8, EUCLID:56 ;
hence ( (f /. i) `1 = (f /. (i + 1)) `1 or (f /. i) `2 = (f /. (i + 1)) `2 ) by A18; :: thesis:

end;

suppose A19: i = 3 ; :: thesis:

(f /. 3) `1 = 1 by A8, EUCLID:56
.= (f /. (3 + 1)) `1 by A9, EUCLID:56 ;
hence ( (f /. i) `1 = (f /. (i + 1)) `1 or (f /. i) `2 = (f /. (i + 1)) `2 ) by A19; :: thesis:

end;

suppose A20: i = 4 ; :: thesis:

(f /. 4) `2 = 0 by A9, EUCLID:56
.= (f /. (4 + 1)) `2 by A10, EUCLID:56 ;
hence ( (f /. i) `1 = (f /. (i + 1)) `1 or (f /. i) `2 = (f /. (i + 1)) `2 ) by A20; :: thesis:

end;

thus f 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 A21: ( 2 < i + 2 & 1 < i + 2 & 0 < i + 2 ) by XXREAL_0:2;
assume i + 2 <= len f ; :: thesis:
then A22: ( i + 2 = 1 + 2 or i + 2 = 2 + 2 or i + 2 = 3 + 2 ) by A2, A21, NAT_1:30;

per cases by A22;

suppose i = 1 ; :: thesis:

hence (LSeg f,i) /\ (LSeg f,(i + 1)) = {(f /. (i + 1))} by A2, A4, A6, A12, TOPREAL1:21, TOPREAL1:def 5; :: thesis:

end;

suppose i = 2 ; :: thesis:

hence (LSeg f,i) /\ (LSeg f,(i + 1)) = {(f /. (i + 1))} by A2, A6, A8, A13, TOPREAL1:24, TOPREAL1:def 5; :: thesis:

end;

suppose i = 3 ; :: thesis:

hence (LSeg f,i) /\ (LSeg f,(i + 1)) = {(f /. (i + 1))} by A2, A8, A9, A14, TOPREAL1:22, TOPREAL1:def 5; :: thesis:

end;

thus f /. 1 = f /. (len f) by A1, A4, A10, FINSEQ_1:35; :: according to FINSEQ_6:def 1 :: thesis:
thus f 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
A23: i + 1 < j and
A24: ( ( i > 1 & j < len f ) or j + 1 < len f ) ; :: thesis:
A25: i + 1 >= 1 by NAT_1:11;
A26: ( 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, A24, NAT_1:30;
A27: (i + 1) + 1 = i + (1 + 1) ;
then A28: i + 2 <= j by A23, NAT_1:13;
A29: ( ( i + 2 = 2 + 2 implies i = 2 ) & ( i + 2 = 1 + 2 implies i = 1 ) & ( i + 2 = 0 + 2 implies i = 0 ) ) ;
A30: i + 2 <> 0 + 1 by A27;

A31: now

per cases by A23, A25, A26, XXREAL_0:2;

case j = 2 ; :: thesis:

hence i = 0 by A23, A27, A29, NAT_1:27; :: thesis:

end;

case j = 3 ; :: thesis:

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

end;

case j = 4 ; :: thesis:

hence ( i = 0 or i = 2 ) by A2, A24, A28, A29, A30, NAT_1:29; :: thesis:

end;

per cases by A31;

suppose i = 0 ; :: thesis:

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

end;

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

hence (LSeg f,i) /\ (LSeg f,j) = {} by A11, A13, TOPREAL1:26, XBOOLE_0:def 7; :: according to XBOOLE_0:def 7 :: thesis:

end;

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

hence (LSeg f,i) /\ (LSeg f,j) = {} by A12, A14, TOPREAL1:25, XBOOLE_0:def 7; :: according to XBOOLE_0:def 7 :: thesis:

end;

set Xf1 = <*0 ,0 ,1*>;
set Xf2 = <*1,0 *>;
reconsider Xf = <*0 ,0 ,1*> ^ <*1,0 *> as FinSequence of REAL ;
A32: ( len <*0 ,0 ,1*> = 3 & len <*1,0 *> = 2 ) by FINSEQ_1:61, FINSEQ_1:62;
then A33: len Xf = 3 + 2 by FINSEQ_1:35;
1 in dom <*0 ,0 ,1*> by A32, FINSEQ_3:27;
then A34: Xf . 1 = <*0 ,0 ,1*> . 1 by FINSEQ_1:def 7
.= 0 by FINSEQ_1:62 ;
2 in dom <*0 ,0 ,1*> by A32, FINSEQ_3:27;
then A35: Xf . 2 = <*0 ,0 ,1*> . 2 by FINSEQ_1:def 7
.= 0 by FINSEQ_1:62 ;
3 in dom <*0 ,0 ,1*> by A32, FINSEQ_3:27;
then A36: Xf . 3 = <*0 ,0 ,1*> . 3 by FINSEQ_1:def 7
.= 1 by FINSEQ_1:62 ;
1 in dom <*1,0 *> by A32, FINSEQ_3:27;
then A37: Xf . (3 + 1) = <*1,0 *> . 1 by A32, FINSEQ_1:def 7
.= 1 by FINSEQ_1:61 ;
2 in dom <*1,0 *> by A32, FINSEQ_3:27;
then A38: Xf . (3 + 2) = <*1,0 *> . 2 by A32, FINSEQ_1:def 7
.= 0 by FINSEQ_1:61 ;

now

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

per cases by A39, NAT_1:30;

suppose n = 1 ; :: thesis:

hence Xf . n = (f /. n) `1 by A4, A34, EUCLID:56; :: thesis:

end;

suppose n = 2 ; :: thesis:

hence Xf . n = (f /. n) `1 by A6, A35, EUCLID:56; :: thesis:

end;

suppose n = 3 ; :: thesis:

hence Xf . n = (f /. n) `1 by A8, A36, EUCLID:56; :: thesis:

end;

suppose n = 4 ; :: thesis:

hence Xf . n = (f /. n) `1 by A9, A37, EUCLID:56; :: thesis:

end;

suppose n = 5 ; :: thesis:

hence Xf . n = (f /. n) `1 by A10, A38, EUCLID:56; :: thesis:

end;

then A40: Xf = X_axis f by A2, A33, GOBOARD1:def 3;
A41: rng <*0 ,0 ,1*> = {0 ,0 ,1} by FINSEQ_2:148
.= {0 ,1} by ENUMSET1:70 ;
rng <*1,0 *> = {0 ,1} by FINSEQ_2:147;
then A42: rng Xf = {0 ,1} \/ {0 ,1} by A41, FINSEQ_1:44
.= {0 ,1} ;
then A43: rng <*0 ,1*> = rng Xf by FINSEQ_2:147;
A44: len <*0 ,1*> = 2 by FINSEQ_1:61
.= card (rng Xf) by A42, CARD_2:76 ;
<*0 ,1*> is increasing

proof

let n, m be Element of NAT ; :: according to SEQM_3:def 1 :: thesis:
len <*0 ,1*> = 2 by FINSEQ_1:61;
then A45: dom <*0 ,1*> = {1,2} by FINSEQ_1:4, FINSEQ_1:def 3;
assume ( n in dom <*0 ,1*> & m in dom <*0 ,1*> ) ; :: thesis:
then A46: ( ( n = 1 or n = 2 ) & ( m = 1 or m = 2 ) ) by A45, TARSKI:def 2;
assume n < m ; :: thesis:
then ( <*0 ,1*> . n = 0 & <*0 ,1*> . m = 1 ) by A46, FINSEQ_1:61;
hence <*0 ,1*> . n < <*0 ,1*> . m ; :: thesis:

end;

then A47: <*0 ,1*> = Incr (X_axis f) by A40, A43, A44, GOBOARD2:def 2;
set Yf1 = <*0 ,1,1*>;
set Yf2 = <*0 ,0 *>;
reconsider Yf = <*0 ,1,1*> ^ <*0 ,0 *> as FinSequence of REAL ;
A48: ( len <*0 ,1,1*> = 3 & len <*0 ,0 *> = 2 ) by FINSEQ_1:61, FINSEQ_1:62;
then A49: len Yf = 3 + 2 by FINSEQ_1:35;
1 in dom <*0 ,1,1*> by A48, FINSEQ_3:27;
then A50: Yf . 1 = <*0 ,1,1*> . 1 by FINSEQ_1:def 7
.= 0 by FINSEQ_1:62 ;
2 in dom <*0 ,1,1*> by A48, FINSEQ_3:27;
then A51: Yf . 2 = <*0 ,1,1*> . 2 by FINSEQ_1:def 7
.= 1 by FINSEQ_1:62 ;
3 in dom <*0 ,1,1*> by A48, FINSEQ_3:27;
then A52: Yf . 3 = <*0 ,1,1*> . 3 by FINSEQ_1:def 7
.= 1 by FINSEQ_1:62 ;
1 in dom <*0 ,0 *> by A48, FINSEQ_3:27;
then A53: Yf . (3 + 1) = <*0 ,0 *> . 1 by A48, FINSEQ_1:def 7
.= 0 by FINSEQ_1:61 ;
2 in dom <*0 ,0 *> by A48, FINSEQ_3:27;
then A54: Yf . (3 + 2) = <*0 ,0 *> . 2 by A48, FINSEQ_1:def 7
.= 0 by FINSEQ_1:61 ;

now

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

per cases by A55, NAT_1:30;

suppose n = 1 ; :: thesis:

hence Yf . n = (f /. n) `2 by A4, A50, EUCLID:56; :: thesis:

end;

suppose n = 2 ; :: thesis:

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

end;

suppose n = 3 ; :: thesis:

hence Yf . n = (f /. n) `2 by A8, A52, EUCLID:56; :: thesis:

end;

suppose n = 4 ; :: thesis:

hence Yf . n = (f /. n) `2 by A9, A53, EUCLID:56; :: thesis:

end;

suppose n = 5 ; :: thesis:

hence Yf . n = (f /. n) `2 by A10, A54, EUCLID:56; :: thesis:

end;

then A56: Yf = Y_axis f by A2, A49, GOBOARD1:def 4;
A57: rng <*0 ,1,1*> = {0 ,1,1} by FINSEQ_2:148
.= {1,1,0 } by ENUMSET1:100
.= {0 ,1} by ENUMSET1:70 ;
rng <*0 ,0 *> = {0 ,0 } by FINSEQ_2:147
.= {0 } by ENUMSET1:69 ;
then A58: rng Yf = {0 ,1} \/ {0 } by A57, FINSEQ_1:44
.= {0 ,0 ,1} by ENUMSET1:42
.= {0 ,1} by ENUMSET1:70 ;
then A59: rng <*0 ,1*> = rng Yf by FINSEQ_2:147;
A60: len <*0 ,1*> = 2 by FINSEQ_1:61
.= card (rng Yf) by A58, CARD_2:76 ;
<*0 ,1*> is increasing

proof

let n, m be Element of NAT ; :: according to SEQM_3:def 1 :: thesis:
len <*0 ,1*> = 2 by FINSEQ_1:61;
then A61: dom <*0 ,1*> = {1,2} by FINSEQ_1:4, FINSEQ_1:def 3;
assume ( n in dom <*0 ,1*> & m in dom <*0 ,1*> ) ; :: thesis:
then A62: ( ( n = 1 or n = 2 ) & ( m = 1 or m = 2 ) ) by A61, TARSKI:def 2;
assume n < m ; :: thesis:
then ( <*0 ,1*> . n = 0 & <*0 ,1*> . m = 1 ) by A62, FINSEQ_1:61;
hence <*0 ,1*> . n < <*0 ,1*> . m ; :: thesis:

end;

then A63: <*0 ,1*> = Incr (Y_axis f) by A56, A59, A60, GOBOARD2:def 2;
set M = |[0 ,0 ]|,|[0 ,1]| ][ |[1,0 ]|,|[1,1]|;
A64: len (|[0 ,0 ]|,|[0 ,1]| ][ |[1,0 ]|,|[1,1]|) = 2 by MATRIX_2:3
.= len (Incr (X_axis f)) by A47, FINSEQ_1:61 ;
A65: width (|[0 ,0 ]|,|[0 ,1]| ][ |[1,0 ]|,|[1,1]|) = 2 by MATRIX_2:3
.= len (Incr (Y_axis f)) by A63, FINSEQ_1:61 ;
for n, m being Element of NAT st [n,m] in Indices (|[0 ,0 ]|,|[0 ,1]| ][ |[1,0 ]|,|[1,1]|) holds
(|[0 ,0 ]|,|[0 ,1]| ][ |[1,0 ]|,|[1,1]|) * n,m = |[((Incr (X_axis f)) . n),((Incr (Y_axis f)) . m)]|

proof

let n, m be Element of NAT ; :: thesis:
assume [n,m] in Indices (|[0 ,0 ]|,|[0 ,1]| ][ |[1,0 ]|,|[1,1]|) ; :: thesis:
then [n,m] in [:{1,2},{1,2}:] by FINSEQ_1:4, MATRIX_2:3;
then A66: [n,m] in {[1,1],[1,2],[2,1],[2,2]} by MCART_1:25;
A67: ( <*0 ,1*> . 1 = 0 & <*0 ,1*> . 2 = 1 ) by FINSEQ_1:61;

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

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

then ( n = 1 & m = 1 ) by ZFMISC_1:33;
hence (|[0 ,0 ]|,|[0 ,1]| ][ |[1,0 ]|,|[1,1]|) * n,m = |[((Incr (X_axis f)) . n),((Incr (Y_axis f)) . m)]| by A47, A63, A67, MATRIX_2:6; :: thesis:

end;

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

then ( n = 1 & m = 2 ) by ZFMISC_1:33;
hence (|[0 ,0 ]|,|[0 ,1]| ][ |[1,0 ]|,|[1,1]|) * n,m = |[((Incr (X_axis f)) . n),((Incr (Y_axis f)) . m)]| by A47, A63, A67, MATRIX_2:6; :: thesis:

end;

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

then ( n = 2 & m = 1 ) by ZFMISC_1:33;
hence (|[0 ,0 ]|,|[0 ,1]| ][ |[1,0 ]|,|[1,1]|) * n,m = |[((Incr (X_axis f)) . n),((Incr (Y_axis f)) . m)]| by A47, A63, A67, MATRIX_2:6; :: thesis:

end;

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

then ( n = 2 & m = 2 ) by ZFMISC_1:33;
hence (|[0 ,0 ]|,|[0 ,1]| ][ |[1,0 ]|,|[1,1]|) * n,m = |[((Incr (X_axis f)) . n),((Incr (Y_axis f)) . m)]| by A47, A63, A67, MATRIX_2:6; :: thesis:

end;

then A68: |[0 ,0 ]|,|[0 ,1]| ][ |[1,0 ]|,|[1,1]| = GoB (Incr (X_axis f)),(Incr (Y_axis f)) by A64, A65, GOBOARD2:def 1
.= GoB f by GOBOARD2:def 3 ;
then A69: f /. 1 = (GoB f) * 1,1 by A4, MATRIX_2:6;
A70: f /. 2 = (GoB f) * 1,2 by A6, A68, MATRIX_2:6;
A71: f /. 3 = (GoB f) * 2,2 by A8, A68, MATRIX_2:6;
A72: f /. 4 = (GoB f) * 2,1 by A9, A68, MATRIX_2:6;
thus for k being Element of NAT st k in dom f holds
ex i, j being Element of NAT st
( [i,j] in Indices (GoB f) & f /. k = (GoB f) * i,j ) :: according to GOBOARD1:def 11,GOBOARD5:def 5 :: thesis:

proof

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

per cases by A74, A75, NAT_1:30;

suppose A76: k = 1 ; :: thesis:

take 1 ; :: thesis:
take 1 ; :: thesis:
thus [1,1] in Indices (GoB f) by A68, MATRIX_2:4; :: thesis:
thus f /. k = (GoB f) * 1,1 by A4, A68, A76, MATRIX_2:6; :: thesis:

end;

suppose A77: k = 2 ; :: thesis:

take 1 ; :: thesis:
take 2 ; :: thesis:
thus [1,2] in Indices (GoB f) by A68, MATRIX_2:4; :: thesis:
thus f /. k = (GoB f) * 1,2 by A6, A68, A77, MATRIX_2:6; :: thesis:

end;

suppose A78: k = 3 ; :: thesis:

take 2 ; :: thesis:
take 2 ; :: thesis:
thus [2,2] in Indices (GoB f) by A68, MATRIX_2:4; :: thesis:
thus f /. k = (GoB f) * 2,2 by A8, A68, A78, MATRIX_2:6; :: thesis:

end;

suppose A79: k = 4 ; :: thesis:

take 2 ; :: thesis:
take 1 ; :: thesis:
thus [2,1] in Indices (GoB f) by A68, MATRIX_2:4; :: thesis:
thus f /. k = (GoB f) * 2,1 by A9, A68, A79, MATRIX_2:6; :: thesis:

end;

suppose A80: k = 5 ; :: thesis:

take 1 ; :: thesis:
take 1 ; :: thesis:
thus [1,1] in Indices (GoB f) by A68, MATRIX_2:4; :: thesis:
thus f /. k = (GoB f) * 1,1 by A10, A68, A80, MATRIX_2:6; :: thesis:

end;

let n be Element of NAT ; :: thesis:
assume that
A81: n in dom f and
A82: n + 1 in dom f ; :: thesis:
let m, k, i, j be Element of NAT ; :: thesis:
assume that
A83: [m,k] in Indices (GoB f) and
A84: [i,j] in Indices (GoB f) and
A85: f /. n = (GoB f) * m,k and
A86: f /. (n + 1) = (GoB f) * 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,1] in Indices (GoB f) by A68, MATRIX_2:4;
then A90: ( m = 1 & k = 1 ) by A69, A83, A85, A89, GOBOARD1:21;
[1,2] in Indices (GoB f) by A68, MATRIX_2:4;
then A91: ( i = 1 & j = 1 + 1 ) by A70, A84, A86, A89, GOBOARD1:21;
then abs (k - j) = 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:

[1,2] in Indices (GoB f) by A68, MATRIX_2:4;
then A93: ( m = 1 & k = 2 ) by A70, A83, A85, A92, GOBOARD1:21;
[2,2] in Indices (GoB f) by A68, MATRIX_2:4;
then A94: ( i = 1 + 1 & j = 2 ) by A71, A84, A86, A92, GOBOARD1:21;
then abs (m - i) = 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,2] in Indices (GoB f) by A68, MATRIX_2:4;
then A96: ( m = 2 & k = 1 + 1 ) by A71, A83, A85, A95, GOBOARD1:21;
[2,1] in Indices (GoB f) by A68, MATRIX_2:4;
then A97: ( i = 2 & j = 1 ) by A72, A84, A86, A95, GOBOARD1:21;
then abs (k - j) = 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:

[2,1] in Indices (GoB f) by A68, MATRIX_2:4;
then A99: ( m = 1 + 1 & k = 1 ) by A72, A83, A85, A98, GOBOARD1:21;
[1,1] in Indices (GoB f) by A68, MATRIX_2:4;
then A100: ( i = 1 & j = 1 ) by A4, A10, A69, A84, A86, A98, GOBOARD1:21;
then abs (m - i) = 1 by A99, GOBOARD1:1;
hence (abs (m - i)) + (abs (k - j)) = 1 by A99, A100, GOBOARD1:2; :: thesis:

end;