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: ( i + 1 = 1 + 1 or i + 1 = 2 + 1 or i + 1 = 3 + 1 or i + 1 = 4 + 1 ) by A3, A17, NAT_1:29;

per cases by 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 A23: 1 + 2 <= i + 2 by XREAL_1:6;
then A24: 2 < i + 2 by XXREAL_0:2;
A25: 1 < i + 2 by A23, XXREAL_0:2;
assume i + 2 <= len f ; :: thesis:
then A26: ( i + 2 = 1 + 2 or i + 2 = 2 + 2 or i + 2 = 3 + 2 ) by A3, A24, A25, NAT_1:29;

per cases by A26;

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 be Element of NAT ; :: according to GOBOARD5:def 4 :: thesis:
let j be Element of NAT ; :: thesis:
assume that
A27: i + 1 < j and
A28: ( ( i > 1 & j < len f ) or j + 1 < len f ) ; :: thesis:
A29: i + 1 >= 1 by NAT_1:11;
A30: ( 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 A3, A28, NAT_1:29;
A31: (i + 1) + 1 = i + (1 + 1) ;
then A32: i + 2 <= j by A27, NAT_1:13;
A33: ( i + 2 = 2 + 2 implies i = 2 ) ;
A34: ( i + 2 = 1 + 2 implies i = 1 ) ;
A35: ( i + 2 = 0 + 2 implies i = 0 ) ;
A36: i + 2 <> 0 + 1 by A31;

A37: now

per cases by A27, A29, A30, XXREAL_0:2;

case j = 2 ; :: thesis:

hence i = 0 by A27, A31, A35, NAT_1:26; :: thesis:

end;

case j = 3 ; :: thesis:

hence ( i = 0 or i = 1 ) by A27, A31, A34, A35, NAT_1:27; :: thesis:

end;

case j = 4 ; :: thesis:

hence ( i = 0 or i = 2 ) by A3, A28, A32, A33, A34, A35, A36, NAT_1:28; :: thesis:

end;

per cases by A37;

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, 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 A14, A16, TOPREAL1:19, 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 ;
A38: len <*0,0,1*> = 3 by FINSEQ_1:45;
A39: len <*1,0*> = 2 by FINSEQ_1:44;
then A40: len Xf = 3 + 2 by A38, FINSEQ_1:22;
1 in dom <*0,0,1*> by A38, FINSEQ_3:25;
then A41: Xf . 1 = <*0,0,1*> . 1 by FINSEQ_1:def 7
.= 0 by FINSEQ_1:45 ;
2 in dom <*0,0,1*> by A38, FINSEQ_3:25;
then A42: Xf . 2 = <*0,0,1*> . 2 by FINSEQ_1:def 7
.= 0 by FINSEQ_1:45 ;
3 in dom <*0,0,1*> by A38, FINSEQ_3:25;
then A43: Xf . 3 = <*0,0,1*> . 3 by FINSEQ_1:def 7
.= 1 by FINSEQ_1:45 ;
1 in dom <*1,0*> by A39, FINSEQ_3:25;
then A44: Xf . (3 + 1) = <*1,0*> . 1 by A38, FINSEQ_1:def 7
.= 1 by FINSEQ_1:44 ;
2 in dom <*1,0*> by A39, FINSEQ_3:25;
then A45: Xf . (3 + 2) = <*1,0*> . 2 by A38, FINSEQ_1:def 7
.= 0 by FINSEQ_1:44 ;

now

let n be Element of NAT ; :: thesis:
assume A46: n in dom Xf ; :: thesis:
then A47: n <> 0 by FINSEQ_3:25;
A48: n <= 5 by A40, A46, FINSEQ_3:25;

per cases by A47, A48, NAT_1:29;

suppose n = 1 ; :: thesis:

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

end;

suppose n = 2 ; :: thesis:

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

end;

suppose n = 3 ; :: thesis:

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

end;

suppose n = 4 ; :: thesis:

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

end;

suppose n = 5 ; :: thesis:

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

end;

then A49: Xf = X_axis f by A3, A40, GOBOARD1:def 1;
A50: rng <*0,0,1*> = {0,0,1} by FINSEQ_2:128
.= {0,1} by ENUMSET1:30 ;
rng <*1,0*> = {0,1} by FINSEQ_2:127;
then A51: rng Xf = {0,1} \/ {0,1} by A50, FINSEQ_1:31
.= {0,1} ;
then A52: rng <*0,1*> = rng Xf by FINSEQ_2:127;
A53: len <*0,1*> = 2 by FINSEQ_1:44
.= card (rng Xf) by A51, CARD_2:57 ;
<*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:44;
then A54: dom <*0,1*> = {1,2} by FINSEQ_1:2, FINSEQ_1:def 3;
assume that
A55: n in dom <*0,1*> and
A56: m in dom <*0,1*> ; :: thesis:
A57: ( n = 1 or n = 2 ) by A54, A55, TARSKI:def 2;
A58: ( m = 1 or m = 2 ) by A54, A56, TARSKI:def 2;
assume A59: n < m ; :: thesis:
then A60: <*0,1*> . n = 0 by A57, A58, FINSEQ_1:44;
<*0,1*> . m = 1 by A57, A58, A59, FINSEQ_1:44;
hence <*0,1*> . n < <*0,1*> . m by A60; :: thesis:

end;

then A61: <*0,1*> = Incr (X_axis f) by A49, A52, A53, SEQ_4:def 21;
set Yf1 = <*0,1,1*>;
set Yf2 = <*0,0*>;
reconsider Yf = <*0,1,1*> ^ <*0,0*> as FinSequence of REAL ;
A62: len <*0,1,1*> = 3 by FINSEQ_1:45;
A63: len <*0,0*> = 2 by FINSEQ_1:44;
then A64: len Yf = 3 + 2 by A62, FINSEQ_1:22;
1 in dom <*0,1,1*> by A62, FINSEQ_3:25;
then A65: Yf . 1 = <*0,1,1*> . 1 by FINSEQ_1:def 7
.= 0 by FINSEQ_1:45 ;
2 in dom <*0,1,1*> by A62, FINSEQ_3:25;
then A66: Yf . 2 = <*0,1,1*> . 2 by FINSEQ_1:def 7
.= 1 by FINSEQ_1:45 ;
3 in dom <*0,1,1*> by A62, FINSEQ_3:25;
then A67: Yf . 3 = <*0,1,1*> . 3 by FINSEQ_1:def 7
.= 1 by FINSEQ_1:45 ;
1 in dom <*0,0*> by A63, FINSEQ_3:25;
then A68: Yf . (3 + 1) = <*0,0*> . 1 by A62, FINSEQ_1:def 7
.= 0 by FINSEQ_1:44 ;
2 in dom <*0,0*> by A63, FINSEQ_3:25;
then A69: Yf . (3 + 2) = <*0,0*> . 2 by A62, FINSEQ_1:def 7
.= 0 by FINSEQ_1:44 ;

now

let n be Element of NAT ; :: thesis:
assume A70: n in dom Yf ; :: thesis:
then A71: n <> 0 by FINSEQ_3:25;
A72: n <= 5 by A64, A70, FINSEQ_3:25;

per cases by A71, A72, NAT_1:29;

suppose n = 1 ; :: thesis:

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

end;

suppose n = 2 ; :: thesis:

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

end;

suppose n = 3 ; :: thesis:

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

end;

suppose n = 4 ; :: thesis:

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

end;

suppose n = 5 ; :: thesis:

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

end;

then A73: Yf = Y_axis f by A3, A64, GOBOARD1:def 2;
A74: rng <*0,1,1*> = {0,1,1} by FINSEQ_2:128
.= {1,1,0} by ENUMSET1:59
.= {0,1} by ENUMSET1:30 ;
rng <*0,0*> = {0,0} by FINSEQ_2:127
.= {0} by ENUMSET1:29 ;
then A75: rng Yf = {0,1} \/ {0} by A74, FINSEQ_1:31
.= {0,0,1} by ENUMSET1:2
.= {0,1} by ENUMSET1:30 ;
then A76: rng <*0,1*> = rng Yf by FINSEQ_2:127;
A77: len <*0,1*> = 2 by FINSEQ_1:44
.= card (rng Yf) by A75, CARD_2:57 ;
<*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:44;
then A78: dom <*0,1*> = {1,2} by FINSEQ_1:2, FINSEQ_1:def 3;
assume that
A79: n in dom <*0,1*> and
A80: m in dom <*0,1*> ; :: thesis:
A81: ( n = 1 or n = 2 ) by A78, A79, TARSKI:def 2;
A82: ( m = 1 or m = 2 ) by A78, A80, TARSKI:def 2;
assume A83: n < m ; :: thesis:
then A84: <*0,1*> . n = 0 by A81, A82, FINSEQ_1:44;
<*0,1*> . m = 1 by A81, A82, A83, FINSEQ_1:44;
hence <*0,1*> . n < <*0,1*> . m by A84; :: thesis:

end;

then A85: <*0,1*> = Incr (Y_axis f) by A73, A76, A77, SEQ_4:def 21;
set M = (|[0,0]|,|[0,1]|) ][ (|[1,0]|,|[1,1]|);
A86: len ((|[0,0]|,|[0,1]|) ][ (|[1,0]|,|[1,1]|)) = 2 by MATRIX_2:3
.= len (Incr (X_axis f)) by A61, FINSEQ_1:44 ;
A87: width ((|[0,0]|,|[0,1]|) ][ (|[1,0]|,|[1,1]|)) = 2 by MATRIX_2:3
.= len (Incr (Y_axis f)) by A85, FINSEQ_1:44 ;
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:2, MATRIX_2:3;
then A88: [n,m] in {[1,1],[1,2],[2,1],[2,2]} by MCART_1:23;
A89: <*0,1*> . 1 = 0 by FINSEQ_1:44;
A90: <*0,1*> . 2 = 1 by FINSEQ_1:44;

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

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

then A92: n = 1 by ZFMISC_1:27;
m = 1 by A91, ZFMISC_1:27;
hence ((|[0,0]|,|[0,1]|) ][ (|[1,0]|,|[1,1]|)) * (n,m) = |[((Incr (X_axis f)) . n),((Incr (Y_axis f)) . m)]| by A61, A85, A89, A92, MATRIX_2:6; :: thesis:

end;

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

then A94: n = 1 by ZFMISC_1:27;
m = 2 by A93, ZFMISC_1:27;
hence ((|[0,0]|,|[0,1]|) ][ (|[1,0]|,|[1,1]|)) * (n,m) = |[((Incr (X_axis f)) . n),((Incr (Y_axis f)) . m)]| by A61, A85, A89, A90, A94, MATRIX_2:6; :: thesis:

end;

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

then A96: n = 2 by ZFMISC_1:27;
m = 1 by A95, ZFMISC_1:27;
hence ((|[0,0]|,|[0,1]|) ][ (|[1,0]|,|[1,1]|)) * (n,m) = |[((Incr (X_axis f)) . n),((Incr (Y_axis f)) . m)]| by A61, A85, A89, A90, A96, MATRIX_2:6; :: thesis:

end;

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

then A98: n = 2 by ZFMISC_1:27;
m = 2 by A97, ZFMISC_1:27;
hence ((|[0,0]|,|[0,1]|) ][ (|[1,0]|,|[1,1]|)) * (n,m) = |[((Incr (X_axis f)) . n),((Incr (Y_axis f)) . m)]| by A61, A85, A90, A98, MATRIX_2:6; :: thesis:

end;

then A99: (|[0,0]|,|[0,1]|) ][ (|[1,0]|,|[1,1]|) = GoB ((Incr (X_axis f)),(Incr (Y_axis f))) by A86, A87, GOBOARD2:def 1
.= GoB f by GOBOARD2:def 2 ;
then A100: f /. 1 = (GoB f) * (1,1) by A5, MATRIX_2:6;
A101: f /. 2 = (GoB f) * (1,2) by A7, A99, MATRIX_2:6;
A102: f /. 3 = (GoB f) * (2,2) by A10, A99, MATRIX_2:6;
A103: f /. 4 = (GoB f) * (2,1) by A11, A99, 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 9,GOBOARD5:def 5 :: thesis:

proof

let k be Element of NAT ; :: thesis:
assume A104: k in dom f ; :: thesis:
then A105: k <= 5 by A3, FINSEQ_3:25;
A106: k <> 0 by A104, FINSEQ_3:25;

per cases by A105, A106, NAT_1:29;

suppose A107: k = 1 ; :: thesis:

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

end;

suppose A108: k = 2 ; :: thesis:

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

end;

suppose A109: k = 3 ; :: thesis:

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

end;

suppose A110: k = 4 ; :: thesis:

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

end;

suppose A111: k = 5 ; :: thesis:

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

end;

let n be Element of NAT ; :: thesis:
assume that
A112: n in dom f and
A113: n + 1 in dom f ; :: thesis:
let m, k, i, j be Element of NAT ; :: thesis:
assume that
A114: [m,k] in Indices (GoB f) and
A115: [i,j] in Indices (GoB f) and
A116: f /. n = (GoB f) * (m,k) and
A117: f /. (n + 1) = (GoB f) * (i,j) ; :: thesis:
A118: n <> 0 by A112, FINSEQ_3:25;
n + 1 <= 4 + 1 by A3, A113, FINSEQ_3:25;
then A119: n <= 4 by XREAL_1:6;

per cases by A118, A119, NAT_1:28;

suppose A120: n = 1 ; :: thesis:

A121: [1,1] in Indices (GoB f) by A99, MATRIX_2:4;
then A122: m = 1 by A100, A114, A116, A120, GOBOARD1:5;
A123: k = 1 by A100, A114, A116, A120, A121, GOBOARD1:5;
A124: [1,2] in Indices (GoB f) by A99, MATRIX_2:4;
then A125: i = 1 by A101, A115, A117, A120, GOBOARD1:5;
j = 1 + 1 by A101, A115, A117, A120, A124, GOBOARD1:5;
then abs (k - j) = 1 by A123, SEQM_3:41;
hence (abs (m - i)) + (abs (k - j)) = 1 by A122, A125, SEQM_3:42; :: thesis:

end;

suppose A126: n = 2 ; :: thesis:

A127: [1,2] in Indices (GoB f) by A99, MATRIX_2:4;
then A128: m = 1 by A101, A114, A116, A126, GOBOARD1:5;
A129: k = 2 by A101, A114, A116, A126, A127, GOBOARD1:5;
A130: [2,2] in Indices (GoB f) by A99, MATRIX_2:4;
then A131: i = 1 + 1 by A102, A115, A117, A126, GOBOARD1:5;
A132: j = 2 by A102, A115, A117, A126, A130, GOBOARD1:5;
abs (m - i) = 1 by A128, A131, SEQM_3:41;
hence (abs (m - i)) + (abs (k - j)) = 1 by A129, A132, SEQM_3:42; :: thesis:

end;

suppose A133: n = 3 ; :: thesis:

A134: [2,2] in Indices (GoB f) by A99, MATRIX_2:4;
then A135: m = 2 by A102, A114, A116, A133, GOBOARD1:5;
A136: k = 1 + 1 by A102, A114, A116, A133, A134, GOBOARD1:5;
A137: [2,1] in Indices (GoB f) by A99, MATRIX_2:4;
then A138: i = 2 by A103, A115, A117, A133, GOBOARD1:5;
j = 1 by A103, A115, A117, A133, A137, GOBOARD1:5;
then abs (k - j) = 1 by A136, SEQM_3:41;
hence (abs (m - i)) + (abs (k - j)) = 1 by A135, A138, SEQM_3:42; :: thesis:

end;

suppose A139: n = 4 ; :: thesis:

A140: [2,1] in Indices (GoB f) by A99, MATRIX_2:4;
then A141: m = 1 + 1 by A103, A114, A116, A139, GOBOARD1:5;
A142: k = 1 by A103, A114, A116, A139, A140, GOBOARD1:5;
A143: [1,1] in Indices (GoB f) by A99, MATRIX_2:4;
then A144: i = 1 by A5, A12, A100, A115, A117, A139, GOBOARD1:5;
A145: j = 1 by A5, A12, A100, A115, A117, A139, A143, GOBOARD1:5;
abs (m - i) = 1 by A141, A144, SEQM_3:41;
hence (abs (m - i)) + (abs (k - j)) = 1 by A142, A145, SEQM_3:42; :: thesis:

end;