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 A17: 1 < i + 1 by XXREAL_0:2;
assume i + 1 <= len f ; :: thesis:
then A18: not not i + 1 = 0 & ... & not i + 1 = 5 by A3;

per cases by A17, A18;

suppose A19: i = 1 ; :: thesis:

(f /. 1) `1 = 0 by A5, EUCLID:52
.= (f /. (1 + 1)) `1 by A7, EUCLID:52 ;
hence ( (f /. i) `1 = (f /. (i + 1)) `1 or (f /. i) `2 = (f /. (i + 1)) `2 ) by A19; :: thesis:

end;

suppose A20: i = 2 ; :: thesis:

(f /. 2) `2 = 1 by A7, EUCLID:52
.= (f /. (2 + 1)) `2 by A10, EUCLID:52 ;
hence ( (f /. i) `1 = (f /. (i + 1)) `1 or (f /. i) `2 = (f /. (i + 1)) `2 ) by A20; :: thesis:

end;

suppose A21: i = 3 ; :: thesis:

(f /. 3) `1 = 1 by A10, EUCLID:52
.= (f /. (3 + 1)) `1 by A11, EUCLID:52 ;
hence ( (f /. i) `1 = (f /. (i + 1)) `1 or (f /. i) `2 = (f /. (i + 1)) `2 ) by A21; :: thesis:

end;

suppose A22: i = 4 ; :: thesis:

(f /. 4) `2 = 0 by A11, EUCLID:52
.= (f /. (4 + 1)) `2 by A12, EUCLID:52 ;
hence ( (f /. i) `1 = (f /. (i + 1)) `1 or (f /. i) `2 = (f /. (i + 1)) `2 ) by A22; :: thesis:

end;

thus f is unfolded :: thesis:

proof

let i be Nat; :: according to TOPREAL1:def 6 :: thesis:
assume 1 <= i ; :: thesis:
then 1 + 2 <= i + 2 by XREAL_1:6;
then A23: 2 < i + 2 by XXREAL_0:2;
assume i + 2 <= len f ; :: thesis:
then A24: not not i + 2 = 0 & ... & not i + 2 = 5 by A3;

per cases by A23, A24;

suppose i = 1 ; :: thesis:

hence (LSeg (f,i)) /\ (LSeg (f,(i + 1))) = {(f /. (i + 1))} by A3, A5, A7, A14, TOPREAL1:15, TOPREAL1:def 3; :: thesis:

end;

suppose i = 2 ; :: thesis:

hence (LSeg (f,i)) /\ (LSeg (f,(i + 1))) = {(f /. (i + 1))} by A3, A7, A10, A15, TOPREAL1:18, TOPREAL1:def 3; :: thesis:

end;

suppose i = 3 ; :: thesis:

hence (LSeg (f,i)) /\ (LSeg (f,(i + 1))) = {(f /. (i + 1))} by A3, A10, A11, A16, TOPREAL1:16, TOPREAL1:def 3; :: thesis:

end;

thus f /. 1 = f /. (len f) by A1, A2, A5, A12, FINSEQ_1:22; :: according to FINSEQ_6:def 1 :: thesis:
thus f is s.c.c. :: thesis:

proof

let i, j be Nat; :: according to GOBOARD5:def 4 :: thesis:
assume that
A25: i + 1 < j and
A26: ( ( i > 1 & j < len f ) or j + 1 < len f ) ; :: thesis:
A27: i + 1 >= 1 by NAT_1:11;
j + 1 <= 5 by A3, A26, NAT_1:13;
then A28: not not j + 1 = 0 & ... & not j + 1 = 5 ;
A29: (i + 1) + 1 = i + (1 + 1) ;
then A30: i + 2 <= j by A25, NAT_1:13;
A31: i + 2 <> 0 + 1 by A29;

A32: now :: thesis:

per cases by A25, A27, A28;

case j = 2 ; :: thesis:

then not not i + 2 = 0 & ... & not i + 2 = 2 by A30;
hence i = 0 by A25; :: thesis:

end;

case j = 3 ; :: thesis:

then not not i + 2 = 0 & ... & not i + 2 = 3 by A30;
hence ( i = 0 or i = 1 ) by A25; :: thesis:

end;

case A33: j = 4 ; :: thesis:

then not not i + 2 = 0 & ... & not i + 2 = 4 by A30;
hence ( i = 0 or i = 2 ) by A3, A26, A31, A33; :: thesis:

end;

per cases by A32;

suppose i = 0 ; :: thesis:

then LSeg (f,i) = {} by TOPREAL1:def 3;
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 A13, A15, TOPREAL1:20; :: according to XBOOLE_0:def 7 :: thesis:

end;

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

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

end;

set Xf1 = <*zz,zz,jj*>;
set Xf2 = <*jj,zz*>;
reconsider Xf = <*zz,zz,jj*> ^ <*jj,zz*> as FinSequence of REAL ;
A34: len <*zz,zz,jj*> = 3 by FINSEQ_1:45;
A35: len <*jj,zz*> = 2 by FINSEQ_1:44;
then A36: len Xf = 3 + 2 by A34, FINSEQ_1:22;
1 in dom <*zz,zz,jj*> by A34, FINSEQ_3:25;
then A37: Xf . 1 = <*zz,zz,jj*> . 1 by FINSEQ_1:def 7
.= 0 ;
2 in dom <*zz,zz,jj*> by A34, FINSEQ_3:25;
then A38: Xf . 2 = <*zz,zz,jj*> . 2 by FINSEQ_1:def 7
.= 0 ;
3 in dom <*zz,zz,jj*> by A34, FINSEQ_3:25;
then A39: Xf . 3 = <*zz,zz,jj*> . 3 by FINSEQ_1:def 7
.= 1 ;
1 in dom <*jj,zz*> by A35, FINSEQ_3:25;
then A40: Xf . (3 + 1) = <*jj,zz*> . 1 by A34, FINSEQ_1:def 7
.= 1 ;
2 in dom <*jj,zz*> by A35, FINSEQ_3:25;
then A41: Xf . (3 + 2) = <*jj,zz*> . 2 by A34, FINSEQ_1:def 7
.= 0 ;

now :: thesis:

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

per cases by A43;

suppose n = 1 ; :: thesis:

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

end;

suppose n = 2 ; :: thesis:

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

end;

suppose n = 3 ; :: thesis:

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

end;

suppose n = 4 ; :: thesis:

hence Xf . n = (f /. n) `1 by A11, A40, EUCLID:52; :: thesis:

end;

suppose n = 5 ; :: thesis:

hence Xf . n = (f /. n) `1 by A12, A41, EUCLID:52; :: thesis:

end;

then A44: Xf = X_axis f by A3, A36, GOBOARD1:def 1;
A45: rng <*zz,zz,jj*> = {0,0,1} by FINSEQ_2:128
.= {0,1} by ENUMSET1:30 ;
rng <*jj,zz*> = {0,1} by FINSEQ_2:127;
then A46: rng Xf = {0,1} \/ {0,1} by A45, FINSEQ_1:31
.= {0,1} ;
then A47: rng <*zz,jj*> = rng Xf by FINSEQ_2:127;
A48: len <*zz,jj*> = 2 by FINSEQ_1:44
.= card (rng Xf) by A46, CARD_2:57 ;
<*zz,jj*> is increasing

proof

let n, m be Nat; :: according to SEQM_3:def 1 :: thesis:
len <*zz,jj*> = 2 by FINSEQ_1:44;
then A49: dom <*zz,jj*> = {1,2} by FINSEQ_1:2, FINSEQ_1:def 3;
assume that
A50: n in dom <*zz,jj*> and
A51: m in dom <*zz,jj*> ; :: thesis:
A52: ( n = 1 or n = 2 ) by A49, A50, TARSKI:def 2;
A53: ( m = 1 or m = 2 ) by A49, A51, TARSKI:def 2;
assume A54: n < m ; :: thesis:
then A55: <*0,jj*> . n = 0 by A52, A53;
<*0,jj*> . m = 1 by A52, A53, A54;
hence <*zz,jj*> . n < <*zz,jj*> . m by A55; :: thesis:

end;

then A56: <*0,jj*> = Incr (X_axis f) by A44, A47, A48, SEQ_4:def 21;
set Yf1 = <*zz,jj,jj*>;
set Yf2 = <*zz,zz*>;
reconsider Yf = <*zz,jj,jj*> ^ <*zz,zz*> as FinSequence of REAL ;
A57: len <*zz,jj,jj*> = 3 by FINSEQ_1:45;
A58: len <*zz,zz*> = 2 by FINSEQ_1:44;
then A59: len Yf = 3 + 2 by A57, FINSEQ_1:22;
1 in dom <*zz,jj,jj*> by A57, FINSEQ_3:25;
then A60: Yf . 1 = <*zz,jj,jj*> . 1 by FINSEQ_1:def 7
.= 0 ;
2 in dom <*zz,jj,jj*> by A57, FINSEQ_3:25;
then A61: Yf . 2 = <*zz,jj,jj*> . 2 by FINSEQ_1:def 7
.= 1 ;
3 in dom <*zz,jj,jj*> by A57, FINSEQ_3:25;
then A62: Yf . 3 = <*zz,jj,jj*> . 3 by FINSEQ_1:def 7
.= 1 ;
1 in dom <*zz,zz*> by A58, FINSEQ_3:25;
then A63: Yf . (3 + 1) = <*zz,zz*> . 1 by A57, FINSEQ_1:def 7
.= 0 ;
2 in dom <*zz,zz*> by A58, FINSEQ_3:25;
then A64: Yf . (3 + 2) = <*zz,zz*> . 2 by A57, FINSEQ_1:def 7
.= 0 ;

now :: thesis:

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

per cases by A66;

suppose n = 1 ; :: thesis:

hence Yf . n = (f /. n) `2 by A5, A60, EUCLID:52; :: thesis:

end;

suppose n = 2 ; :: thesis:

hence Yf . n = (f /. n) `2 by A7, A61, EUCLID:52; :: thesis:

end;

suppose n = 3 ; :: thesis:

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

end;

suppose n = 4 ; :: thesis:

hence Yf . n = (f /. n) `2 by A11, A63, EUCLID:52; :: thesis:

end;

suppose n = 5 ; :: thesis:

hence Yf . n = (f /. n) `2 by A12, A64, EUCLID:52; :: thesis:

end;

then A67: Yf = Y_axis f by A3, A59, GOBOARD1:def 2;
A68: rng <*zz,jj,jj*> = {0,1,1} by FINSEQ_2:128
.= {1,1,0} by ENUMSET1:59
.= {0,1} by ENUMSET1:30 ;
rng <*zz,zz*> = {0,0} by FINSEQ_2:127
.= {0} by ENUMSET1:29 ;
then A69: rng Yf = {0,1} \/ {0} by A68, FINSEQ_1:31
.= {0,0,1} by ENUMSET1:2
.= {0,1} by ENUMSET1:30 ;
then A70: rng <*0,jj*> = rng Yf by FINSEQ_2:127;
A71: len <*0,jj*> = 2 by FINSEQ_1:44
.= card (rng Yf) by A69, CARD_2:57 ;
<*(In (0,REAL)),jj*> is increasing

proof

let n, m be Nat; :: according to SEQM_3:def 1 :: thesis:
len <*0,jj*> = 2 by FINSEQ_1:44;
then A72: dom <*0,jj*> = {1,2} by FINSEQ_1:2, FINSEQ_1:def 3;
assume that
A73: n in dom <*(In (0,REAL)),jj*> and
A74: m in dom <*(In (0,REAL)),jj*> ; :: thesis:
A75: ( n = 1 or n = 2 ) by A72, A73, TARSKI:def 2;
A76: ( m = 1 or m = 2 ) by A72, A74, TARSKI:def 2;
assume A77: n < m ; :: thesis:
then A78: <*0,jj*> . n = 0 by A75, A76;
<*0,jj*> . m = 1 by A75, A76, A77;
hence <*(In (0,REAL)),jj*> . n < <*(In (0,REAL)),jj*> . m by A78; :: thesis:

end;

then A79: <*0,jj*> = Incr (Y_axis f) by A67, A70, A71, SEQ_4:def 21;
set M = (|[0,0]|,|[0,1]|) ][ (|[1,0]|,|[1,1]|);
A80: len ((|[0,0]|,|[0,1]|) ][ (|[1,0]|,|[1,1]|)) = 2 by MATRIX_0:47
.= len (Incr (X_axis f)) by A56, FINSEQ_1:44 ;
A81: width ((|[0,0]|,|[0,1]|) ][ (|[1,0]|,|[1,1]|)) = 2 by MATRIX_0:47
.= len (Incr (Y_axis f)) by A79, FINSEQ_1:44 ;
for n, m being 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 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:2, MATRIX_0:47;
then A82: [n,m] in {[1,1],[1,2],[2,1],[2,2]} by MCART_1:23;

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

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

then A86: n = 1 by XTUPLE_0:1;
m = 1 by A85, XTUPLE_0:1;
hence ((|[0,0]|,|[0,1]|) ][ (|[1,0]|,|[1,1]|)) * (n,m) = |[((Incr (X_axis f)) . n),((Incr (Y_axis f)) . m)]| by A56, A79, A86, MATRIX_0:50; :: thesis:

end;

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

then A88: n = 1 by XTUPLE_0:1;
m = 2 by A87, XTUPLE_0:1;
hence ((|[0,0]|,|[0,1]|) ][ (|[1,0]|,|[1,1]|)) * (n,m) = |[((Incr (X_axis f)) . n),((Incr (Y_axis f)) . m)]| by A56, A79, A88, MATRIX_0:50; :: thesis:

end;

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

then A90: n = 2 by XTUPLE_0:1;
m = 1 by A89, XTUPLE_0:1;
hence ((|[0,0]|,|[0,1]|) ][ (|[1,0]|,|[1,1]|)) * (n,m) = |[((Incr (X_axis f)) . n),((Incr (Y_axis f)) . m)]| by A56, A79, A90, MATRIX_0:50; :: thesis:

end;

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

then A92: n = 2 by XTUPLE_0:1;
m = 2 by A91, XTUPLE_0:1;
hence ((|[0,0]|,|[0,1]|) ][ (|[1,0]|,|[1,1]|)) * (n,m) = |[((Incr (X_axis f)) . n),((Incr (Y_axis f)) . m)]| by A56, A79, A92, MATRIX_0:50; :: thesis:

end;

then A93: (|[0,0]|,|[0,1]|) ][ (|[1,0]|,|[1,1]|) = GoB ((Incr (X_axis f)),(Incr (Y_axis f))) by A80, A81, GOBOARD2:def 1
.= GoB f by GOBOARD2:def 2 ;
then A94: f /. 1 = (GoB f) * (1,1) by A5, MATRIX_0:50;
A95: f /. 2 = (GoB f) * (1,2) by A7, A93, MATRIX_0:50;
A96: f /. 3 = (GoB f) * (2,2) by A10, A93, MATRIX_0:50;
A97: f /. 4 = (GoB f) * (2,1) by A11, A93, MATRIX_0:50;
thus for k being Nat st k in dom f holds
ex i, j being Nat st
( [i,j] in Indices (GoB f) & f /. k = (GoB f) * (i,j) ) :: according to GOBOARD1:def 9,GOBOARD5:def 5 :: thesis:

proof

let k be Nat; :: thesis:
assume A98: k in dom f ; :: thesis:
then A99: k <= 5 by A3, FINSEQ_3:25;
A100: k <> 0 by A98, FINSEQ_3:25;
not not k = 0 & ... & not k = 5 by A99;

per cases by A100;

suppose A101: k = 1 ; :: thesis:

take 1 ; :: thesis:
take 1 ; :: thesis:
thus [1,1] in Indices (GoB f) by A93, MATRIX_0:48; :: thesis:
thus f /. k = (GoB f) * (1,1) by A5, A93, A101, MATRIX_0:50; :: thesis:

end;

suppose A102: k = 2 ; :: thesis:

take 1 ; :: thesis:
take 2 ; :: thesis:
thus [1,2] in Indices (GoB f) by A93, MATRIX_0:48; :: thesis:
thus f /. k = (GoB f) * (1,2) by A7, A93, A102, MATRIX_0:50; :: thesis:

end;

suppose A103: k = 3 ; :: thesis:

take 2 ; :: thesis:
take 2 ; :: thesis:
thus [2,2] in Indices (GoB f) by A93, MATRIX_0:48; :: thesis:
thus f /. k = (GoB f) * (2,2) by A10, A93, A103, MATRIX_0:50; :: thesis:

end;

suppose A104: k = 4 ; :: thesis:

take 2 ; :: thesis:
take 1 ; :: thesis:
thus [2,1] in Indices (GoB f) by A93, MATRIX_0:48; :: thesis:
thus f /. k = (GoB f) * (2,1) by A11, A93, A104, MATRIX_0:50; :: thesis:

end;

suppose A105: k = 5 ; :: thesis:

take 1 ; :: thesis:
take 1 ; :: thesis:
thus [1,1] in Indices (GoB f) by A93, MATRIX_0:48; :: thesis:
thus f /. k = (GoB f) * (1,1) by A12, A93, A105, MATRIX_0:50; :: thesis:

end;

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

per cases by A112;

suppose A113: n = 1 ; :: thesis:

A114: [1,1] in Indices (GoB f) by A93, MATRIX_0:48;
then A115: m = 1 by A94, A108, A110, A113, GOBOARD1:5;
A116: k = 1 by A94, A108, A110, A113, A114, GOBOARD1:5;
A117: [1,2] in Indices (GoB f) by A93, MATRIX_0:48;
then A118: i = 1 by A95, A109, A111, A113, GOBOARD1:5;
j = 1 + 1 by A95, A109, A111, A113, A117, GOBOARD1:5;
then |.(k - j).| = 1 by A116, SEQM_3:41;
hence |.(m - i).| + |.(k - j).| = 1 by A115, A118, SEQM_3:42; :: thesis:

end;

suppose A119: n = 2 ; :: thesis:

A120: [1,2] in Indices (GoB f) by A93, MATRIX_0:48;
then A121: m = 1 by A95, A108, A110, A119, GOBOARD1:5;
A122: k = 2 by A95, A108, A110, A119, A120, GOBOARD1:5;
A123: [2,2] in Indices (GoB f) by A93, MATRIX_0:48;
then A124: i = 1 + 1 by A96, A109, A111, A119, GOBOARD1:5;
A125: j = 2 by A96, A109, A111, A119, A123, GOBOARD1:5;
|.(m - i).| = 1 by A121, A124, SEQM_3:41;
hence |.(m - i).| + |.(k - j).| = 1 by A122, A125, SEQM_3:42; :: thesis:

end;

suppose A126: n = 3 ; :: thesis:

A127: [2,2] in Indices (GoB f) by A93, MATRIX_0:48;
then A128: m = 2 by A96, A108, A110, A126, GOBOARD1:5;
A129: k = 1 + 1 by A96, A108, A110, A126, A127, GOBOARD1:5;
A130: [2,1] in Indices (GoB f) by A93, MATRIX_0:48;
then A131: i = 2 by A97, A109, A111, A126, GOBOARD1:5;
j = 1 by A97, A109, A111, A126, A130, GOBOARD1:5;
then |.(k - j).| = 1 by A129, SEQM_3:41;
hence |.(m - i).| + |.(k - j).| = 1 by A128, A131, SEQM_3:42; :: thesis:

end;

suppose A132: n = 4 ; :: thesis:

A133: [2,1] in Indices (GoB f) by A93, MATRIX_0:48;
then A134: m = 1 + 1 by A97, A108, A110, A132, GOBOARD1:5;
A135: k = 1 by A97, A108, A110, A132, A133, GOBOARD1:5;
A136: [1,1] in Indices (GoB f) by A93, MATRIX_0:48;
then A137: i = 1 by A5, A12, A94, A109, A111, A132, GOBOARD1:5;
A138: j = 1 by A5, A12, A94, A109, A111, A132, A136, GOBOARD1:5;
|.(m - i).| = 1 by A134, A137, SEQM_3:41;
hence |.(m - i).| + |.(k - j).| = 1 by A135, A138, SEQM_3:42; :: thesis:

end;