let f be FinSequence of (TOP-REAL 2); :: thesis: for G being Go-board st ( for n being Nat st n in dom f holds

ex i, j being Nat st

( [i,j] in Indices G & f /. n = G * (i,j) ) ) & f is special & ( for n being Nat st n in dom f & n + 1 in dom f holds

f /. n <> f /. (n + 1) ) holds

ex g being FinSequence of (TOP-REAL 2) st

( g is_sequence_on G & L~ f = L~ g & g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g )

let G be Go-board; :: thesis: ( ( for n being Nat st n in dom f holds

ex i, j being Nat st

( [i,j] in Indices G & f /. n = G * (i,j) ) ) & f is special & ( for n being Nat st n in dom f & n + 1 in dom f holds

f /. n <> f /. (n + 1) ) implies ex g being FinSequence of (TOP-REAL 2) st

( g is_sequence_on G & L~ f = L~ g & g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g ) )

defpred S_{1}[ Nat] means for f being FinSequence of (TOP-REAL 2) st len f = $1 & ( for n being Nat st n in dom f holds

ex i, j being Nat st

( [i,j] in Indices G & f /. n = G * (i,j) ) ) & f is special & ( for n being Nat st n in dom f & n + 1 in dom f holds

f /. n <> f /. (n + 1) ) holds

ex g being FinSequence of (TOP-REAL 2) st

( g is_sequence_on G & L~ f = L~ g & g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g );

A1: for k being Nat st S_{1}[k] holds

S_{1}[k + 1]

ex i, j being Nat st

( [i,j] in Indices G & f /. n = G * (i,j) ) ) & f is special & ( for n being Nat st n in dom f & n + 1 in dom f holds

f /. n <> f /. (n + 1) ) holds

ex g being FinSequence of (TOP-REAL 2) st

( g is_sequence_on G & L~ f = L~ g & g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g )

let G be Go-board; :: thesis: ( ( for n being Nat st n in dom f holds

ex i, j being Nat st

( [i,j] in Indices G & f /. n = G * (i,j) ) ) & f is special & ( for n being Nat st n in dom f & n + 1 in dom f holds

f /. n <> f /. (n + 1) ) implies ex g being FinSequence of (TOP-REAL 2) st

( g is_sequence_on G & L~ f = L~ g & g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g ) )

defpred S

ex i, j being Nat st

( [i,j] in Indices G & f /. n = G * (i,j) ) ) & f is special & ( for n being Nat st n in dom f & n + 1 in dom f holds

f /. n <> f /. (n + 1) ) holds

ex g being FinSequence of (TOP-REAL 2) st

( g is_sequence_on G & L~ f = L~ g & g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g );

A1: for k being Nat st S

S

proof

let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A2: S_{1}[k]
; :: thesis: S_{1}[k + 1]

let f be FinSequence of (TOP-REAL 2); :: thesis: ( len f = k + 1 & ( for n being Nat st n in dom f holds

ex i, j being Nat st

( [i,j] in Indices G & f /. n = G * (i,j) ) ) & f is special & ( for n being Nat st n in dom f & n + 1 in dom f holds

f /. n <> f /. (n + 1) ) implies ex g being FinSequence of (TOP-REAL 2) st

( g is_sequence_on G & L~ f = L~ g & g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g ) )

assume that

A3: len f = k + 1 and

A4: for n being Nat st n in dom f holds

ex i, j being Nat st

( [i,j] in Indices G & f /. n = G * (i,j) ) and

A5: f is special and

A6: for n being Nat st n in dom f & n + 1 in dom f holds

f /. n <> f /. (n + 1) ; :: thesis: ex g being FinSequence of (TOP-REAL 2) st

( g is_sequence_on G & L~ f = L~ g & g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g )

A7: dom f = Seg (len f) by FINSEQ_1:def 3;

assume A2: S

let f be FinSequence of (TOP-REAL 2); :: thesis: ( len f = k + 1 & ( for n being Nat st n in dom f holds

ex i, j being Nat st

( [i,j] in Indices G & f /. n = G * (i,j) ) ) & f is special & ( for n being Nat st n in dom f & n + 1 in dom f holds

f /. n <> f /. (n + 1) ) implies ex g being FinSequence of (TOP-REAL 2) st

( g is_sequence_on G & L~ f = L~ g & g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g ) )

assume that

A3: len f = k + 1 and

A4: for n being Nat st n in dom f holds

ex i, j being Nat st

( [i,j] in Indices G & f /. n = G * (i,j) ) and

A5: f is special and

A6: for n being Nat st n in dom f & n + 1 in dom f holds

f /. n <> f /. (n + 1) ; :: thesis: ex g being FinSequence of (TOP-REAL 2) st

( g is_sequence_on G & L~ f = L~ g & g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g )

A7: dom f = Seg (len f) by FINSEQ_1:def 3;

now :: thesis: ex g being FinSequence of (TOP-REAL 2) st

( g is_sequence_on G & L~ f = L~ g & g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g )

( g is_sequence_on G & L~ f = L~ g & g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g )

per cases
( k = 0 or k <> 0 )
;

suppose A8:
k = 0
; :: thesis: ex g being FinSequence of (TOP-REAL 2) st

( g is_sequence_on G & L~ f = L~ g & g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g )

( g is_sequence_on G & L~ f = L~ g & g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g )

take g = f; :: thesis: ( g is_sequence_on G & L~ f = L~ g & g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g )

A9: dom f = {1} by A3, A8, FINSEQ_1:2, FINSEQ_1:def 3;

thus ( L~ f = L~ g & g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g ) ; :: thesis: verum

end;A9: dom f = {1} by A3, A8, FINSEQ_1:2, FINSEQ_1:def 3;

now :: thesis: for n being Nat st n in dom g & n + 1 in dom g holds

for i1, i2, j1, j2 being Nat st [i1,i2] in Indices G & [j1,j2] in Indices G & g /. n = G * (i1,i2) & g /. (n + 1) = G * (j1,j2) holds

|.(i1 - j1).| + |.(i2 - j2).| = 1

hence
g is_sequence_on G
by A4; :: thesis: ( L~ f = L~ g & g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g )for i1, i2, j1, j2 being Nat st [i1,i2] in Indices G & [j1,j2] in Indices G & g /. n = G * (i1,i2) & g /. (n + 1) = G * (j1,j2) holds

|.(i1 - j1).| + |.(i2 - j2).| = 1

let n be Nat; :: thesis: ( n in dom g & n + 1 in dom g implies for i1, i2, j1, j2 being Nat st [i1,i2] in Indices G & [j1,j2] in Indices G & g /. n = G * (i1,i2) & g /. (n + 1) = G * (j1,j2) holds

|.(i1 - j1).| + |.(i2 - j2).| = 1 )

assume that

A10: n in dom g and

A11: n + 1 in dom g ; :: thesis: for i1, i2, j1, j2 being Nat st [i1,i2] in Indices G & [j1,j2] in Indices G & g /. n = G * (i1,i2) & g /. (n + 1) = G * (j1,j2) holds

|.(i1 - j1).| + |.(i2 - j2).| = 1

n = 1 by A9, A10, TARSKI:def 1;

hence for i1, i2, j1, j2 being Nat st [i1,i2] in Indices G & [j1,j2] in Indices G & g /. n = G * (i1,i2) & g /. (n + 1) = G * (j1,j2) holds

|.(i1 - j1).| + |.(i2 - j2).| = 1 by A9, A11, TARSKI:def 1; :: thesis: verum

end;|.(i1 - j1).| + |.(i2 - j2).| = 1 )

assume that

A10: n in dom g and

A11: n + 1 in dom g ; :: thesis: for i1, i2, j1, j2 being Nat st [i1,i2] in Indices G & [j1,j2] in Indices G & g /. n = G * (i1,i2) & g /. (n + 1) = G * (j1,j2) holds

|.(i1 - j1).| + |.(i2 - j2).| = 1

n = 1 by A9, A10, TARSKI:def 1;

hence for i1, i2, j1, j2 being Nat st [i1,i2] in Indices G & [j1,j2] in Indices G & g /. n = G * (i1,i2) & g /. (n + 1) = G * (j1,j2) holds

|.(i1 - j1).| + |.(i2 - j2).| = 1 by A9, A11, TARSKI:def 1; :: thesis: verum

thus ( L~ f = L~ g & g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g ) ; :: thesis: verum

suppose A12:
k <> 0
; :: thesis: ex g being FinSequence of (TOP-REAL 2) st

( g is_sequence_on G & L~ f = L~ g & g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g )

( g is_sequence_on G & L~ f = L~ g & g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g )

then A13:
0 + 1 <= k
by NAT_1:13;

then A14: k in Seg k by FINSEQ_1:1;

A15: 1 in Seg k by A13, FINSEQ_1:1;

A16: k <= k + 1 by NAT_1:11;

then A17: k in dom f by A3, A7, A13, FINSEQ_1:1;

then consider i1, i2 being Nat such that

A18: [i1,i2] in Indices G and

A19: f /. k = G * (i1,i2) by A4;

reconsider l1 = Line (G,i1), c1 = Col (G,i2) as FinSequence of (TOP-REAL 2) ;

set x1 = X_axis l1;

set y1 = Y_axis l1;

set x2 = X_axis c1;

set y2 = Y_axis c1;

A20: ( dom (Y_axis l1) = Seg (len (Y_axis l1)) & len (Y_axis l1) = len l1 ) by FINSEQ_1:def 3, GOBOARD1:def 2;

len (Y_axis c1) = len c1 by GOBOARD1:def 2;

then A21: dom (Y_axis c1) = dom c1 by FINSEQ_3:29;

len (X_axis c1) = len c1 by GOBOARD1:def 1;

then A22: dom (X_axis c1) = dom c1 by FINSEQ_3:29;

set f1 = f | k;

A23: len (f | k) = k by A3, FINSEQ_1:59, NAT_1:11;

A24: dom (f | k) = Seg (len (f | k)) by FINSEQ_1:def 3;

A35: g1 is_sequence_on G and

A36: L~ g1 = L~ (f | k) and

A37: g1 /. 1 = (f | k) /. 1 and

A38: g1 /. (len g1) = (f | k) /. (len (f | k)) and

A39: len (f | k) <= len g1 by A2, A23, A25, A28;

A40: for n being Nat st n in dom g1 holds

ex m, k being Nat st

( [m,k] in Indices G & g1 /. n = G * (m,k) ) by A35;

A41: for n being Nat st n in dom g1 & n + 1 in dom g1 holds

for m, k, i, j being Nat st [m,k] in Indices G & [i,j] in Indices G & g1 /. n = G * (m,k) & g1 /. (n + 1) = G * (i,j) holds

|.(m - i).| + |.(k - j).| = 1 by A35;

A42: ( dom (X_axis l1) = Seg (len (X_axis l1)) & len (X_axis l1) = len l1 ) by FINSEQ_1:def 3, GOBOARD1:def 1;

len c1 = len G by MATRIX_0:def 8;

then A43: dom c1 = dom G by FINSEQ_3:29;

1 <= len f by A3, NAT_1:11;

then A44: k + 1 in dom f by A3, FINSEQ_3:25;

then consider j1, j2 being Nat such that

A45: [j1,j2] in Indices G and

A46: f /. (k + 1) = G * (j1,j2) by A4;

A47: Indices G = [:(dom G),(Seg (width G)):] by MATRIX_0:def 4;

then A48: j1 in dom G by A45, ZFMISC_1:87;

A49: i1 in dom G by A18, A47, ZFMISC_1:87;

then A50: X_axis l1 is constant by GOBOARD1:def 4;

A51: i2 in Seg (width G) by A18, A47, ZFMISC_1:87;

then A52: X_axis c1 is increasing by GOBOARD1:def 7;

A53: Y_axis c1 is constant by A51, GOBOARD1:def 5;

A54: Y_axis l1 is increasing by A49, GOBOARD1:def 6;

A55: len l1 = width G by MATRIX_0:def 7;

A56: j2 in Seg (width G) by A45, A47, ZFMISC_1:87;

A57: dom g1 = Seg (len g1) by FINSEQ_1:def 3;

then A14: k in Seg k by FINSEQ_1:1;

A15: 1 in Seg k by A13, FINSEQ_1:1;

A16: k <= k + 1 by NAT_1:11;

then A17: k in dom f by A3, A7, A13, FINSEQ_1:1;

then consider i1, i2 being Nat such that

A18: [i1,i2] in Indices G and

A19: f /. k = G * (i1,i2) by A4;

reconsider l1 = Line (G,i1), c1 = Col (G,i2) as FinSequence of (TOP-REAL 2) ;

set x1 = X_axis l1;

set y1 = Y_axis l1;

set x2 = X_axis c1;

set y2 = Y_axis c1;

A20: ( dom (Y_axis l1) = Seg (len (Y_axis l1)) & len (Y_axis l1) = len l1 ) by FINSEQ_1:def 3, GOBOARD1:def 2;

len (Y_axis c1) = len c1 by GOBOARD1:def 2;

then A21: dom (Y_axis c1) = dom c1 by FINSEQ_3:29;

len (X_axis c1) = len c1 by GOBOARD1:def 1;

then A22: dom (X_axis c1) = dom c1 by FINSEQ_3:29;

set f1 = f | k;

A23: len (f | k) = k by A3, FINSEQ_1:59, NAT_1:11;

A24: dom (f | k) = Seg (len (f | k)) by FINSEQ_1:def 3;

A25: now :: thesis: for n being Nat st n in dom (f | k) holds

ex i, j being Nat st

( [i,j] in Indices G & (f | k) /. n = G * (i,j) )

A28:
f | k is special
ex i, j being Nat st

( [i,j] in Indices G & (f | k) /. n = G * (i,j) )

let n be Nat; :: thesis: ( n in dom (f | k) implies ex i, j being Nat st

( [i,j] in Indices G & (f | k) /. n = G * (i,j) ) )

assume A26: n in dom (f | k) ; :: thesis: ex i, j being Nat st

( [i,j] in Indices G & (f | k) /. n = G * (i,j) )

then n in dom f by A17, A23, A24, FINSEQ_4:71;

then consider i, j being Nat such that

A27: ( [i,j] in Indices G & f /. n = G * (i,j) ) by A4;

take i = i; :: thesis: ex j being Nat st

( [i,j] in Indices G & (f | k) /. n = G * (i,j) )

take j = j; :: thesis: ( [i,j] in Indices G & (f | k) /. n = G * (i,j) )

thus ( [i,j] in Indices G & (f | k) /. n = G * (i,j) ) by A17, A23, A24, A26, A27, FINSEQ_4:71; :: thesis: verum

end;( [i,j] in Indices G & (f | k) /. n = G * (i,j) ) )

assume A26: n in dom (f | k) ; :: thesis: ex i, j being Nat st

( [i,j] in Indices G & (f | k) /. n = G * (i,j) )

then n in dom f by A17, A23, A24, FINSEQ_4:71;

then consider i, j being Nat such that

A27: ( [i,j] in Indices G & f /. n = G * (i,j) ) by A4;

take i = i; :: thesis: ex j being Nat st

( [i,j] in Indices G & (f | k) /. n = G * (i,j) )

take j = j; :: thesis: ( [i,j] in Indices G & (f | k) /. n = G * (i,j) )

thus ( [i,j] in Indices G & (f | k) /. n = G * (i,j) ) by A17, A23, A24, A26, A27, FINSEQ_4:71; :: thesis: verum

proof

let n be Nat; :: according to TOPREAL1:def 5 :: thesis: ( not 1 <= n or not n + 1 <= len (f | k) or ((f | k) /. n) `1 = ((f | k) /. (n + 1)) `1 or ((f | k) /. n) `2 = ((f | k) /. (n + 1)) `2 )

assume that

A29: 1 <= n and

A30: n + 1 <= len (f | k) ; :: thesis: ( ((f | k) /. n) `1 = ((f | k) /. (n + 1)) `1 or ((f | k) /. n) `2 = ((f | k) /. (n + 1)) `2 )

n <= n + 1 by NAT_1:11;

then n <= len (f | k) by A30, XXREAL_0:2;

then n in dom (f | k) by A29, FINSEQ_3:25;

then A31: (f | k) /. n = f /. n by A17, A23, A24, FINSEQ_4:71;

1 <= n + 1 by NAT_1:11;

then n + 1 in dom (f | k) by A30, FINSEQ_3:25;

then A32: (f | k) /. (n + 1) = f /. (n + 1) by A17, A23, A24, FINSEQ_4:71;

n + 1 <= len f by A3, A16, A23, A30, XXREAL_0:2;

hence ( ((f | k) /. n) `1 = ((f | k) /. (n + 1)) `1 or ((f | k) /. n) `2 = ((f | k) /. (n + 1)) `2 ) by A5, A29, A31, A32; :: thesis: verum

end;assume that

A29: 1 <= n and

A30: n + 1 <= len (f | k) ; :: thesis: ( ((f | k) /. n) `1 = ((f | k) /. (n + 1)) `1 or ((f | k) /. n) `2 = ((f | k) /. (n + 1)) `2 )

n <= n + 1 by NAT_1:11;

then n <= len (f | k) by A30, XXREAL_0:2;

then n in dom (f | k) by A29, FINSEQ_3:25;

then A31: (f | k) /. n = f /. n by A17, A23, A24, FINSEQ_4:71;

1 <= n + 1 by NAT_1:11;

then n + 1 in dom (f | k) by A30, FINSEQ_3:25;

then A32: (f | k) /. (n + 1) = f /. (n + 1) by A17, A23, A24, FINSEQ_4:71;

n + 1 <= len f by A3, A16, A23, A30, XXREAL_0:2;

hence ( ((f | k) /. n) `1 = ((f | k) /. (n + 1)) `1 or ((f | k) /. n) `2 = ((f | k) /. (n + 1)) `2 ) by A5, A29, A31, A32; :: thesis: verum

now :: thesis: for n being Nat st n in dom (f | k) & n + 1 in dom (f | k) holds

(f | k) /. n <> (f | k) /. (n + 1)

then consider g1 being FinSequence of (TOP-REAL 2) such that (f | k) /. n <> (f | k) /. (n + 1)

let n be Nat; :: thesis: ( n in dom (f | k) & n + 1 in dom (f | k) implies (f | k) /. n <> (f | k) /. (n + 1) )

assume A33: ( n in dom (f | k) & n + 1 in dom (f | k) ) ; :: thesis: (f | k) /. n <> (f | k) /. (n + 1)

then A34: ( (f | k) /. n = f /. n & (f | k) /. (n + 1) = f /. (n + 1) ) by A17, A23, A24, FINSEQ_4:71;

( n in dom f & n + 1 in dom f ) by A17, A23, A24, A33, FINSEQ_4:71;

hence (f | k) /. n <> (f | k) /. (n + 1) by A6, A34; :: thesis: verum

end;assume A33: ( n in dom (f | k) & n + 1 in dom (f | k) ) ; :: thesis: (f | k) /. n <> (f | k) /. (n + 1)

then A34: ( (f | k) /. n = f /. n & (f | k) /. (n + 1) = f /. (n + 1) ) by A17, A23, A24, FINSEQ_4:71;

( n in dom f & n + 1 in dom f ) by A17, A23, A24, A33, FINSEQ_4:71;

hence (f | k) /. n <> (f | k) /. (n + 1) by A6, A34; :: thesis: verum

A35: g1 is_sequence_on G and

A36: L~ g1 = L~ (f | k) and

A37: g1 /. 1 = (f | k) /. 1 and

A38: g1 /. (len g1) = (f | k) /. (len (f | k)) and

A39: len (f | k) <= len g1 by A2, A23, A25, A28;

A40: for n being Nat st n in dom g1 holds

ex m, k being Nat st

( [m,k] in Indices G & g1 /. n = G * (m,k) ) by A35;

A41: for n being Nat st n in dom g1 & n + 1 in dom g1 holds

for m, k, i, j being Nat st [m,k] in Indices G & [i,j] in Indices G & g1 /. n = G * (m,k) & g1 /. (n + 1) = G * (i,j) holds

|.(m - i).| + |.(k - j).| = 1 by A35;

A42: ( dom (X_axis l1) = Seg (len (X_axis l1)) & len (X_axis l1) = len l1 ) by FINSEQ_1:def 3, GOBOARD1:def 1;

len c1 = len G by MATRIX_0:def 8;

then A43: dom c1 = dom G by FINSEQ_3:29;

1 <= len f by A3, NAT_1:11;

then A44: k + 1 in dom f by A3, FINSEQ_3:25;

then consider j1, j2 being Nat such that

A45: [j1,j2] in Indices G and

A46: f /. (k + 1) = G * (j1,j2) by A4;

A47: Indices G = [:(dom G),(Seg (width G)):] by MATRIX_0:def 4;

then A48: j1 in dom G by A45, ZFMISC_1:87;

A49: i1 in dom G by A18, A47, ZFMISC_1:87;

then A50: X_axis l1 is constant by GOBOARD1:def 4;

A51: i2 in Seg (width G) by A18, A47, ZFMISC_1:87;

then A52: X_axis c1 is increasing by GOBOARD1:def 7;

A53: Y_axis c1 is constant by A51, GOBOARD1:def 5;

A54: Y_axis l1 is increasing by A49, GOBOARD1:def 6;

A55: len l1 = width G by MATRIX_0:def 7;

A56: j2 in Seg (width G) by A45, A47, ZFMISC_1:87;

A57: dom g1 = Seg (len g1) by FINSEQ_1:def 3;

now :: thesis: ex g being FinSequence of (TOP-REAL 2) st

( g is_sequence_on G & L~ f = L~ g & g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g )

( g is_sequence_on G & L~ f = L~ g & g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g )

per cases
( i1 = j1 or i2 = j2 )
by A5, A17, A18, A19, A44, A45, A46, Th11;

suppose A58:
i1 = j1
; :: thesis: ex g being FinSequence of (TOP-REAL 2) st

( g is_sequence_on G & L~ f = L~ g & g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g )

( g is_sequence_on G & L~ f = L~ g & g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g )

set ppi = G * (i1,i2);

set pj = G * (i1,j2);

( g is_sequence_on G & L~ f = L~ g & g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g ) ; :: thesis: verum

end;set pj = G * (i1,j2);

now :: thesis: ( ( i2 > j2 & ex g being FinSequence of the carrier of (TOP-REAL 2) st

( g is_sequence_on G & L~ g = L~ f & g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g ) ) or ( i2 = j2 & contradiction ) or ( i2 < j2 & ex g being FinSequence of the carrier of (TOP-REAL 2) st

( g is_sequence_on G & L~ g = L~ f & g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g ) ) )end;

hence
ex g being FinSequence of (TOP-REAL 2) st ( g is_sequence_on G & L~ g = L~ f & g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g ) ) or ( i2 = j2 & contradiction ) or ( i2 < j2 & ex g being FinSequence of the carrier of (TOP-REAL 2) st

( g is_sequence_on G & L~ g = L~ f & g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g ) ) )

per cases
( i2 > j2 or i2 = j2 or i2 < j2 )
by XXREAL_0:1;

end;

case A59:
i2 > j2
; :: thesis: ex g being FinSequence of the carrier of (TOP-REAL 2) st

( g is_sequence_on G & L~ g = L~ f & g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g )

( g is_sequence_on G & L~ g = L~ f & g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g )

j2 in dom l1
by A56, A55, FINSEQ_1:def 3;

then l1 /. j2 = l1 . j2 by PARTFUN1:def 6;

then A60: l1 /. j2 = G * (i1,j2) by A56, MATRIX_0:def 7;

then A61: (Y_axis l1) . j2 = (G * (i1,j2)) `2 by A56, A20, A55, GOBOARD1:def 2;

i2 in dom l1 by A51, A55, FINSEQ_1:def 3;

then l1 /. i2 = l1 . i2 by PARTFUN1:def 6;

then A62: l1 /. i2 = G * (i1,i2) by A51, MATRIX_0:def 7;

then A63: (Y_axis l1) . i2 = (G * (i1,i2)) `2 by A51, A20, A55, GOBOARD1:def 2;

then A64: (G * (i1,j2)) `2 < (G * (i1,i2)) `2 by A51, A56, A54, A20, A55, A59, A61, SEQM_3:def 1;

A65: (X_axis l1) . j2 = (G * (i1,j2)) `1 by A56, A42, A55, A60, GOBOARD1:def 1;

(X_axis l1) . i2 = (G * (i1,i2)) `1 by A51, A42, A55, A62, GOBOARD1:def 1;

then A66: (G * (i1,i2)) `1 = (G * (i1,j2)) `1 by A51, A56, A50, A42, A55, A65, SEQM_3:def 10;

reconsider l = i2 - j2 as Element of NAT by A59, INT_1:5;

defpred S_{2}[ Nat, set ] means for m being Nat st m = i2 - $1 holds

$2 = G * (i1,m);

set lk = { w where w is Point of (TOP-REAL 2) : ( w `1 = (G * (i1,i2)) `1 & (G * (i1,j2)) `2 <= w `2 & w `2 <= (G * (i1,i2)) `2 ) } ;

A67: G * (i1,i2) = |[((G * (i1,i2)) `1),((G * (i1,i2)) `2)]| by EUCLID:53;

A73: ( len g2 = l & ( for n being Nat st n in Seg l holds

S_{2}[n,g2 /. n] ) )
from FINSEQ_4:sch 1(A72);

take g = g1 ^ g2; :: thesis: ( g is_sequence_on G & L~ g = L~ f & g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g )

A74: dom g2 = Seg l by A73, FINSEQ_1:def 3;

ex i, j being Nat st

( [i,j] in Indices G & g /. n = G * (i,j) ) by A40, GOBOARD1:23;

for m, k, i, j being Nat st [m,k] in Indices G & [i,j] in Indices G & g /. n = G * (m,k) & g /. (n + 1) = G * (i,j) holds

|.(m - i).| + |.(k - j).| = 1 by A41, A75, GOBOARD1:24;

hence g is_sequence_on G by A84; :: thesis: ( L~ g = L~ f & g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g )

reconsider m1 = i2 - l as Element of NAT by ORDINAL1:def 12;

A91: G * (i1,j2) = |[((G * (i1,j2)) `1),((G * (i1,j2)) `2)]| by EUCLID:53;

A92: LSeg (f,k) = LSeg ((G * (i1,j2)),(G * (i1,i2))) by A3, A13, A19, A46, A58, TOPREAL1:def 3

.= { w where w is Point of (TOP-REAL 2) : ( w `1 = (G * (i1,i2)) `1 & (G * (i1,j2)) `2 <= w `2 & w `2 <= (G * (i1,i2)) `2 ) } by A64, A66, A67, A91, TOPREAL3:9 ;

thus L~ g = L~ f :: thesis: ( g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g )

then 1 in dom g1 by FINSEQ_3:25;

hence g /. 1 = (f | k) /. 1 by A37, FINSEQ_4:68

.= f /. 1 by A17, A15, FINSEQ_4:71 ;

:: thesis: ( g /. (len g) = f /. (len f) & len f <= len g )

A173: len g = (len g1) + (len g2) by FINSEQ_1:22;

j2 + 1 <= i2 by A59, NAT_1:13;

then A174: 1 <= l by XREAL_1:19;

then A175: l in dom g2 by A74, FINSEQ_1:1;

hence g /. (len g) = g2 /. l by A73, A173, FINSEQ_4:69

.= G * (i1,m1) by A73, A74, A175

.= f /. (len f) by A3, A46, A58 ;

:: thesis: len f <= len g

thus len f <= len g by A3, A23, A39, A73, A174, A173, XREAL_1:7; :: thesis: verum

end;then l1 /. j2 = l1 . j2 by PARTFUN1:def 6;

then A60: l1 /. j2 = G * (i1,j2) by A56, MATRIX_0:def 7;

then A61: (Y_axis l1) . j2 = (G * (i1,j2)) `2 by A56, A20, A55, GOBOARD1:def 2;

i2 in dom l1 by A51, A55, FINSEQ_1:def 3;

then l1 /. i2 = l1 . i2 by PARTFUN1:def 6;

then A62: l1 /. i2 = G * (i1,i2) by A51, MATRIX_0:def 7;

then A63: (Y_axis l1) . i2 = (G * (i1,i2)) `2 by A51, A20, A55, GOBOARD1:def 2;

then A64: (G * (i1,j2)) `2 < (G * (i1,i2)) `2 by A51, A56, A54, A20, A55, A59, A61, SEQM_3:def 1;

A65: (X_axis l1) . j2 = (G * (i1,j2)) `1 by A56, A42, A55, A60, GOBOARD1:def 1;

(X_axis l1) . i2 = (G * (i1,i2)) `1 by A51, A42, A55, A62, GOBOARD1:def 1;

then A66: (G * (i1,i2)) `1 = (G * (i1,j2)) `1 by A51, A56, A50, A42, A55, A65, SEQM_3:def 10;

reconsider l = i2 - j2 as Element of NAT by A59, INT_1:5;

defpred S

$2 = G * (i1,m);

set lk = { w where w is Point of (TOP-REAL 2) : ( w `1 = (G * (i1,i2)) `1 & (G * (i1,j2)) `2 <= w `2 & w `2 <= (G * (i1,i2)) `2 ) } ;

A67: G * (i1,i2) = |[((G * (i1,i2)) `1),((G * (i1,i2)) `2)]| by EUCLID:53;

A68: now :: thesis: for n being Nat st n in Seg l holds

( i2 - n is Element of NAT & [i1,(i2 - n)] in Indices G & i2 - n in Seg (width G) )

( i2 - n is Element of NAT & [i1,(i2 - n)] in Indices G & i2 - n in Seg (width G) )

let n be Nat; :: thesis: ( n in Seg l implies ( i2 - n is Element of NAT & [i1,(i2 - n)] in Indices G & i2 - n in Seg (width G) ) )

assume n in Seg l ; :: thesis: ( i2 - n is Element of NAT & [i1,(i2 - n)] in Indices G & i2 - n in Seg (width G) )

then A69: n <= l by FINSEQ_1:1;

l <= i2 by XREAL_1:43;

then reconsider w = i2 - n as Element of NAT by A69, INT_1:5, XXREAL_0:2;

( i2 - n <= i2 & i2 <= width G ) by A51, FINSEQ_1:1, XREAL_1:43;

then A70: w <= width G by XXREAL_0:2;

A71: 1 <= j2 by A56, FINSEQ_1:1;

i2 - l <= i2 - n by A69, XREAL_1:13;

then 1 <= w by A71, XXREAL_0:2;

then w in Seg (width G) by A70, FINSEQ_1:1;

hence ( i2 - n is Element of NAT & [i1,(i2 - n)] in Indices G & i2 - n in Seg (width G) ) by A47, A49, ZFMISC_1:87; :: thesis: verum

end;assume n in Seg l ; :: thesis: ( i2 - n is Element of NAT & [i1,(i2 - n)] in Indices G & i2 - n in Seg (width G) )

then A69: n <= l by FINSEQ_1:1;

l <= i2 by XREAL_1:43;

then reconsider w = i2 - n as Element of NAT by A69, INT_1:5, XXREAL_0:2;

( i2 - n <= i2 & i2 <= width G ) by A51, FINSEQ_1:1, XREAL_1:43;

then A70: w <= width G by XXREAL_0:2;

A71: 1 <= j2 by A56, FINSEQ_1:1;

i2 - l <= i2 - n by A69, XREAL_1:13;

then 1 <= w by A71, XXREAL_0:2;

then w in Seg (width G) by A70, FINSEQ_1:1;

hence ( i2 - n is Element of NAT & [i1,(i2 - n)] in Indices G & i2 - n in Seg (width G) ) by A47, A49, ZFMISC_1:87; :: thesis: verum

A72: now :: thesis: for n being Nat st n in Seg l holds

ex p being Element of the carrier of (TOP-REAL 2) st S_{2}[n,p]

consider g2 being FinSequence of (TOP-REAL 2) such that ex p being Element of the carrier of (TOP-REAL 2) st S

let n be Nat; :: thesis: ( n in Seg l implies ex p being Element of the carrier of (TOP-REAL 2) st S_{2}[n,p] )

assume n in Seg l ; :: thesis: ex p being Element of the carrier of (TOP-REAL 2) st S_{2}[n,p]

then reconsider m = i2 - n as Element of NAT by A68;

take p = G * (i1,m); :: thesis: S_{2}[n,p]

thus S_{2}[n,p]
; :: thesis: verum

end;assume n in Seg l ; :: thesis: ex p being Element of the carrier of (TOP-REAL 2) st S

then reconsider m = i2 - n as Element of NAT by A68;

take p = G * (i1,m); :: thesis: S

thus S

A73: ( len g2 = l & ( for n being Nat st n in Seg l holds

S

take g = g1 ^ g2; :: thesis: ( g is_sequence_on G & L~ g = L~ f & g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g )

A74: dom g2 = Seg l by A73, FINSEQ_1:def 3;

A75: now :: thesis: for n being Nat st n in dom g2 & n + 1 in dom g2 holds

for l1, l2, l3, l4 being Nat st [l1,l2] in Indices G & [l3,l4] in Indices G & g2 /. n = G * (l1,l2) & g2 /. (n + 1) = G * (l3,l4) holds

|.(l1 - l3).| + |.(l2 - l4).| = 1

for l1, l2, l3, l4 being Nat st [l1,l2] in Indices G & [l3,l4] in Indices G & g2 /. n = G * (l1,l2) & g2 /. (n + 1) = G * (l3,l4) holds

|.(l1 - l3).| + |.(l2 - l4).| = 1

let n be Nat; :: thesis: ( n in dom g2 & n + 1 in dom g2 implies for l1, l2, l3, l4 being Nat st [l1,l2] in Indices G & [l3,l4] in Indices G & g2 /. n = G * (l1,l2) & g2 /. (n + 1) = G * (l3,l4) holds

|.(l1 - l3).| + |.(l2 - l4).| = 1 )

assume that

A76: n in dom g2 and

A77: n + 1 in dom g2 ; :: thesis: for l1, l2, l3, l4 being Nat st [l1,l2] in Indices G & [l3,l4] in Indices G & g2 /. n = G * (l1,l2) & g2 /. (n + 1) = G * (l3,l4) holds

|.(l1 - l3).| + |.(l2 - l4).| = 1

reconsider m1 = i2 - n, m2 = i2 - (n + 1) as Element of NAT by A68, A74, A76, A77;

let l1, l2, l3, l4 be Nat; :: thesis: ( [l1,l2] in Indices G & [l3,l4] in Indices G & g2 /. n = G * (l1,l2) & g2 /. (n + 1) = G * (l3,l4) implies |.(l1 - l3).| + |.(l2 - l4).| = 1 )

assume that

A78: [l1,l2] in Indices G and

A79: [l3,l4] in Indices G and

A80: g2 /. n = G * (l1,l2) and

A81: g2 /. (n + 1) = G * (l3,l4) ; :: thesis: |.(l1 - l3).| + |.(l2 - l4).| = 1

( [i1,(i2 - (n + 1))] in Indices G & g2 /. (n + 1) = G * (i1,m2) ) by A68, A73, A74, A77;

then A82: ( l3 = i1 & l4 = m2 ) by A79, A81, GOBOARD1:5;

( [i1,(i2 - n)] in Indices G & g2 /. n = G * (i1,m1) ) by A68, A73, A74, A76;

then ( l1 = i1 & l2 = m1 ) by A78, A80, GOBOARD1:5;

hence |.(l1 - l3).| + |.(l2 - l4).| = 0 + |.((i2 - n) - (i2 - (n + 1))).| by A82, ABSVALUE:2

.= 1 by ABSVALUE:def 1 ;

:: thesis: verum

end;|.(l1 - l3).| + |.(l2 - l4).| = 1 )

assume that

A76: n in dom g2 and

A77: n + 1 in dom g2 ; :: thesis: for l1, l2, l3, l4 being Nat st [l1,l2] in Indices G & [l3,l4] in Indices G & g2 /. n = G * (l1,l2) & g2 /. (n + 1) = G * (l3,l4) holds

|.(l1 - l3).| + |.(l2 - l4).| = 1

reconsider m1 = i2 - n, m2 = i2 - (n + 1) as Element of NAT by A68, A74, A76, A77;

let l1, l2, l3, l4 be Nat; :: thesis: ( [l1,l2] in Indices G & [l3,l4] in Indices G & g2 /. n = G * (l1,l2) & g2 /. (n + 1) = G * (l3,l4) implies |.(l1 - l3).| + |.(l2 - l4).| = 1 )

assume that

A78: [l1,l2] in Indices G and

A79: [l3,l4] in Indices G and

A80: g2 /. n = G * (l1,l2) and

A81: g2 /. (n + 1) = G * (l3,l4) ; :: thesis: |.(l1 - l3).| + |.(l2 - l4).| = 1

( [i1,(i2 - (n + 1))] in Indices G & g2 /. (n + 1) = G * (i1,m2) ) by A68, A73, A74, A77;

then A82: ( l3 = i1 & l4 = m2 ) by A79, A81, GOBOARD1:5;

( [i1,(i2 - n)] in Indices G & g2 /. n = G * (i1,m1) ) by A68, A73, A74, A76;

then ( l1 = i1 & l2 = m1 ) by A78, A80, GOBOARD1:5;

hence |.(l1 - l3).| + |.(l2 - l4).| = 0 + |.((i2 - n) - (i2 - (n + 1))).| by A82, ABSVALUE:2

.= 1 by ABSVALUE:def 1 ;

:: thesis: verum

now :: thesis: for n being Nat st n in dom g2 holds

ex k, m being Nat st

( [k,m] in Indices G & g2 /. n = G * (k,m) )

then A84:
for n being Nat st n in dom g holds ex k, m being Nat st

( [k,m] in Indices G & g2 /. n = G * (k,m) )

let n be Nat; :: thesis: ( n in dom g2 implies ex k, m being Nat st

( [k,m] in Indices G & g2 /. n = G * (k,m) ) )

assume A83: n in dom g2 ; :: thesis: ex k, m being Nat st

( [k,m] in Indices G & g2 /. n = G * (k,m) )

then reconsider m = i2 - n as Element of NAT by A68, A74;

reconsider k = i1, m = m as Nat ;

take k = k; :: thesis: ex m being Nat st

( [k,m] in Indices G & g2 /. n = G * (k,m) )

take m = m; :: thesis: ( [k,m] in Indices G & g2 /. n = G * (k,m) )

thus ( [k,m] in Indices G & g2 /. n = G * (k,m) ) by A68, A73, A74, A83; :: thesis: verum

end;( [k,m] in Indices G & g2 /. n = G * (k,m) ) )

assume A83: n in dom g2 ; :: thesis: ex k, m being Nat st

( [k,m] in Indices G & g2 /. n = G * (k,m) )

then reconsider m = i2 - n as Element of NAT by A68, A74;

reconsider k = i1, m = m as Nat ;

take k = k; :: thesis: ex m being Nat st

( [k,m] in Indices G & g2 /. n = G * (k,m) )

take m = m; :: thesis: ( [k,m] in Indices G & g2 /. n = G * (k,m) )

thus ( [k,m] in Indices G & g2 /. n = G * (k,m) ) by A68, A73, A74, A83; :: thesis: verum

ex i, j being Nat st

( [i,j] in Indices G & g /. n = G * (i,j) ) by A40, GOBOARD1:23;

now :: thesis: for l1, l2, l3, l4 being Nat st [l1,l2] in Indices G & [l3,l4] in Indices G & g1 /. (len g1) = G * (l1,l2) & g2 /. 1 = G * (l3,l4) & len g1 in dom g1 & 1 in dom g2 holds

|.(l1 - l3).| + |.(l2 - l4).| = 1

then
for n being Nat st n in dom g & n + 1 in dom g holds |.(l1 - l3).| + |.(l2 - l4).| = 1

let l1, l2, l3, l4 be Nat; :: thesis: ( [l1,l2] in Indices G & [l3,l4] in Indices G & g1 /. (len g1) = G * (l1,l2) & g2 /. 1 = G * (l3,l4) & len g1 in dom g1 & 1 in dom g2 implies |.(l1 - l3).| + |.(l2 - l4).| = 1 )

assume that

A85: [l1,l2] in Indices G and

A86: [l3,l4] in Indices G and

A87: g1 /. (len g1) = G * (l1,l2) and

A88: g2 /. 1 = G * (l3,l4) and

len g1 in dom g1 and

A89: 1 in dom g2 ; :: thesis: |.(l1 - l3).| + |.(l2 - l4).| = 1

reconsider m1 = i2 - 1 as Element of NAT by A68, A74, A89;

( [i1,(i2 - 1)] in Indices G & g2 /. 1 = G * (i1,m1) ) by A68, A73, A74, A89;

then A90: ( l3 = i1 & l4 = m1 ) by A86, A88, GOBOARD1:5;

(f | k) /. (len (f | k)) = f /. k by A17, A23, A14, FINSEQ_4:71;

then ( l1 = i1 & l2 = i2 ) by A38, A18, A19, A85, A87, GOBOARD1:5;

hence |.(l1 - l3).| + |.(l2 - l4).| = 0 + |.(i2 - (i2 - 1)).| by A90, ABSVALUE:2

.= 1 by ABSVALUE:def 1 ;

:: thesis: verum

end;assume that

A85: [l1,l2] in Indices G and

A86: [l3,l4] in Indices G and

A87: g1 /. (len g1) = G * (l1,l2) and

A88: g2 /. 1 = G * (l3,l4) and

len g1 in dom g1 and

A89: 1 in dom g2 ; :: thesis: |.(l1 - l3).| + |.(l2 - l4).| = 1

reconsider m1 = i2 - 1 as Element of NAT by A68, A74, A89;

( [i1,(i2 - 1)] in Indices G & g2 /. 1 = G * (i1,m1) ) by A68, A73, A74, A89;

then A90: ( l3 = i1 & l4 = m1 ) by A86, A88, GOBOARD1:5;

(f | k) /. (len (f | k)) = f /. k by A17, A23, A14, FINSEQ_4:71;

then ( l1 = i1 & l2 = i2 ) by A38, A18, A19, A85, A87, GOBOARD1:5;

hence |.(l1 - l3).| + |.(l2 - l4).| = 0 + |.(i2 - (i2 - 1)).| by A90, ABSVALUE:2

.= 1 by ABSVALUE:def 1 ;

:: thesis: verum

for m, k, i, j being Nat st [m,k] in Indices G & [i,j] in Indices G & g /. n = G * (m,k) & g /. (n + 1) = G * (i,j) holds

|.(m - i).| + |.(k - j).| = 1 by A41, A75, GOBOARD1:24;

hence g is_sequence_on G by A84; :: thesis: ( L~ g = L~ f & g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g )

reconsider m1 = i2 - l as Element of NAT by ORDINAL1:def 12;

A91: G * (i1,j2) = |[((G * (i1,j2)) `1),((G * (i1,j2)) `2)]| by EUCLID:53;

A92: LSeg (f,k) = LSeg ((G * (i1,j2)),(G * (i1,i2))) by A3, A13, A19, A46, A58, TOPREAL1:def 3

.= { w where w is Point of (TOP-REAL 2) : ( w `1 = (G * (i1,i2)) `1 & (G * (i1,j2)) `2 <= w `2 & w `2 <= (G * (i1,i2)) `2 ) } by A64, A66, A67, A91, TOPREAL3:9 ;

thus L~ g = L~ f :: thesis: ( g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g )

proof

1 <= len g1
by A13, A23, A39, XXREAL_0:2;
set lg = { (LSeg (g,i)) where i is Nat : ( 1 <= i & i + 1 <= len g ) } ;

set lf = { (LSeg (f,j)) where j is Nat : ( 1 <= j & j + 1 <= len f ) } ;

A93: len g = (len g1) + (len g2) by FINSEQ_1:22;

assume x in L~ f ; :: thesis: x in L~ g

then A141: x in (L~ (f | k)) \/ (LSeg (f,k)) by A3, A12, Th3;

end;set lf = { (LSeg (f,j)) where j is Nat : ( 1 <= j & j + 1 <= len f ) } ;

A93: len g = (len g1) + (len g2) by FINSEQ_1:22;

A94: now :: thesis: for j being Nat st len g1 <= j & j <= len g holds

for p being Point of (TOP-REAL 2) st p = g /. j holds

( p `1 = (G * (i1,i2)) `1 & (G * (i1,j2)) `2 <= p `2 & p `2 <= (G * (i1,i2)) `2 & p in rng l1 )

thus
L~ g c= L~ f
:: according to XBOOLE_0:def 10 :: thesis: L~ f c= L~ gfor p being Point of (TOP-REAL 2) st p = g /. j holds

( p `1 = (G * (i1,i2)) `1 & (G * (i1,j2)) `2 <= p `2 & p `2 <= (G * (i1,i2)) `2 & p in rng l1 )

let j be Nat; :: thesis: ( len g1 <= j & j <= len g implies for p being Point of (TOP-REAL 2) st p = g /. j holds

( p `1 = (G * (i1,i2)) `1 & (G * (i1,j2)) `2 <= p `2 & p `2 <= (G * (i1,i2)) `2 & p in rng l1 ) )

assume that

A95: len g1 <= j and

A96: j <= len g ; :: thesis: for p being Point of (TOP-REAL 2) st p = g /. j holds

( p `1 = (G * (i1,i2)) `1 & (G * (i1,j2)) `2 <= p `2 & p `2 <= (G * (i1,i2)) `2 & p in rng l1 )

reconsider w = j - (len g1) as Element of NAT by A95, INT_1:5;

let p be Point of (TOP-REAL 2); :: thesis: ( p = g /. j implies ( p `1 = (G * (i1,i2)) `1 & (G * (i1,j2)) `2 <= p `2 & p `2 <= (G * (i1,i2)) `2 & p in rng l1 ) )

assume A97: p = g /. j ; :: thesis: ( p `1 = (G * (i1,i2)) `1 & (G * (i1,j2)) `2 <= p `2 & p `2 <= (G * (i1,i2)) `2 & p in rng l1 )

A98: dom l1 = Seg (len l1) by FINSEQ_1:def 3;

end;( p `1 = (G * (i1,i2)) `1 & (G * (i1,j2)) `2 <= p `2 & p `2 <= (G * (i1,i2)) `2 & p in rng l1 ) )

assume that

A95: len g1 <= j and

A96: j <= len g ; :: thesis: for p being Point of (TOP-REAL 2) st p = g /. j holds

( p `1 = (G * (i1,i2)) `1 & (G * (i1,j2)) `2 <= p `2 & p `2 <= (G * (i1,i2)) `2 & p in rng l1 )

reconsider w = j - (len g1) as Element of NAT by A95, INT_1:5;

let p be Point of (TOP-REAL 2); :: thesis: ( p = g /. j implies ( p `1 = (G * (i1,i2)) `1 & (G * (i1,j2)) `2 <= p `2 & p `2 <= (G * (i1,i2)) `2 & p in rng l1 ) )

assume A97: p = g /. j ; :: thesis: ( p `1 = (G * (i1,i2)) `1 & (G * (i1,j2)) `2 <= p `2 & p `2 <= (G * (i1,i2)) `2 & p in rng l1 )

A98: dom l1 = Seg (len l1) by FINSEQ_1:def 3;

now :: thesis: ( p `1 = (G * (i1,i2)) `1 & (G * (i1,j2)) `2 <= p `2 & p `2 <= (G * (i1,i2)) `2 & p in rng l1 )end;

hence
( p `1 = (G * (i1,i2)) `1 & (G * (i1,j2)) `2 <= p `2 & p `2 <= (G * (i1,i2)) `2 & p in rng l1 )
; :: thesis: verumper cases
( j = len g1 or j <> len g1 )
;

end;

suppose A99:
j = len g1
; :: thesis: ( p `1 = (G * (i1,i2)) `1 & (G * (i1,j2)) `2 <= p `2 & p `2 <= (G * (i1,i2)) `2 & p in rng l1 )

1 <= len g1
by A13, A23, A39, XXREAL_0:2;

then len g1 in dom g1 by FINSEQ_3:25;

then A100: g /. (len g1) = (f | k) /. (len (f | k)) by A38, FINSEQ_4:68

.= G * (i1,i2) by A17, A23, A14, A19, FINSEQ_4:71 ;

hence p `1 = (G * (i1,i2)) `1 by A97, A99; :: thesis: ( (G * (i1,j2)) `2 <= p `2 & p `2 <= (G * (i1,i2)) `2 & p in rng l1 )

thus ( (G * (i1,j2)) `2 <= p `2 & p `2 <= (G * (i1,i2)) `2 ) by A51, A56, A54, A20, A55, A59, A63, A61, A97, A99, A100, SEQM_3:def 1; :: thesis: p in rng l1

thus p in rng l1 by A51, A55, A62, A97, A98, A99, A100, PARTFUN2:2; :: thesis: verum

end;then len g1 in dom g1 by FINSEQ_3:25;

then A100: g /. (len g1) = (f | k) /. (len (f | k)) by A38, FINSEQ_4:68

.= G * (i1,i2) by A17, A23, A14, A19, FINSEQ_4:71 ;

hence p `1 = (G * (i1,i2)) `1 by A97, A99; :: thesis: ( (G * (i1,j2)) `2 <= p `2 & p `2 <= (G * (i1,i2)) `2 & p in rng l1 )

thus ( (G * (i1,j2)) `2 <= p `2 & p `2 <= (G * (i1,i2)) `2 ) by A51, A56, A54, A20, A55, A59, A63, A61, A97, A99, A100, SEQM_3:def 1; :: thesis: p in rng l1

thus p in rng l1 by A51, A55, A62, A97, A98, A99, A100, PARTFUN2:2; :: thesis: verum

suppose A101:
j <> len g1
; :: thesis: ( p `1 = (G * (i1,i2)) `1 & (G * (i1,j2)) `2 <= p `2 & p `2 <= (G * (i1,i2)) `2 & p in rng l1 )

A102:
w + (len g1) = j
;

then A103: w <= len g2 by A93, A96, XREAL_1:6;

A104: j - (len g1) <> 0 by A101;

then A105: w >= 1 by NAT_1:14;

then A106: w in dom g2 by A103, FINSEQ_3:25;

then reconsider u = i2 - w as Element of NAT by A68, A74;

A107: g /. j = g2 /. w by A105, A102, A103, SEQ_4:136;

A108: (X_axis l1) . i2 = (G * (i1,i2)) `1 by A51, A42, A55, A62, GOBOARD1:def 1;

A109: u < i2 by A104, XREAL_1:44;

A110: g2 /. w = G * (i1,u) by A73, A74, A106;

A111: i2 - w in Seg (width G) by A68, A74, A106;

then u in dom l1 by A55, FINSEQ_1:def 3;

then l1 /. u = l1 . u by PARTFUN1:def 6;

then A112: l1 /. u = G * (i1,u) by A111, MATRIX_0:def 7;

then A113: (Y_axis l1) . u = (G * (i1,u)) `2 by A20, A55, A111, GOBOARD1:def 2;

(X_axis l1) . u = (G * (i1,u)) `1 by A42, A55, A111, A112, GOBOARD1:def 1;

hence p `1 = (G * (i1,i2)) `1 by A51, A50, A42, A55, A97, A107, A111, A110, A108, SEQM_3:def 10; :: thesis: ( (G * (i1,j2)) `2 <= p `2 & p `2 <= (G * (i1,i2)) `2 & p in rng l1 )

A114: (Y_axis l1) . j2 = (G * (i1,j2)) `2 by A56, A20, A55, A60, GOBOARD1:def 2;

(Y_axis l1) . i2 = (G * (i1,i2)) `2 by A51, A20, A55, A62, GOBOARD1:def 2;

hence p `2 <= (G * (i1,i2)) `2 by A51, A54, A20, A55, A97, A107, A111, A110, A113, A109, SEQM_3:def 1; :: thesis: p in rng l1

thus p in rng l1 by A55, A97, A98, A107, A111, A110, A112, PARTFUN2:2; :: thesis: verum

end;then A103: w <= len g2 by A93, A96, XREAL_1:6;

A104: j - (len g1) <> 0 by A101;

then A105: w >= 1 by NAT_1:14;

then A106: w in dom g2 by A103, FINSEQ_3:25;

then reconsider u = i2 - w as Element of NAT by A68, A74;

A107: g /. j = g2 /. w by A105, A102, A103, SEQ_4:136;

A108: (X_axis l1) . i2 = (G * (i1,i2)) `1 by A51, A42, A55, A62, GOBOARD1:def 1;

A109: u < i2 by A104, XREAL_1:44;

A110: g2 /. w = G * (i1,u) by A73, A74, A106;

A111: i2 - w in Seg (width G) by A68, A74, A106;

then u in dom l1 by A55, FINSEQ_1:def 3;

then l1 /. u = l1 . u by PARTFUN1:def 6;

then A112: l1 /. u = G * (i1,u) by A111, MATRIX_0:def 7;

then A113: (Y_axis l1) . u = (G * (i1,u)) `2 by A20, A55, A111, GOBOARD1:def 2;

(X_axis l1) . u = (G * (i1,u)) `1 by A42, A55, A111, A112, GOBOARD1:def 1;

hence p `1 = (G * (i1,i2)) `1 by A51, A50, A42, A55, A97, A107, A111, A110, A108, SEQM_3:def 10; :: thesis: ( (G * (i1,j2)) `2 <= p `2 & p `2 <= (G * (i1,i2)) `2 & p in rng l1 )

A114: (Y_axis l1) . j2 = (G * (i1,j2)) `2 by A56, A20, A55, A60, GOBOARD1:def 2;

now :: thesis: (G * (i1,j2)) `2 <= p `2 end;

hence
(G * (i1,j2)) `2 <= p `2
; :: thesis: ( p `2 <= (G * (i1,i2)) `2 & p in rng l1 )(Y_axis l1) . i2 = (G * (i1,i2)) `2 by A51, A20, A55, A62, GOBOARD1:def 2;

hence p `2 <= (G * (i1,i2)) `2 by A51, A54, A20, A55, A97, A107, A111, A110, A113, A109, SEQM_3:def 1; :: thesis: p in rng l1

thus p in rng l1 by A55, A97, A98, A107, A111, A110, A112, PARTFUN2:2; :: thesis: verum

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in L~ f or x in L~ g )
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in L~ g or x in L~ f )

assume x in L~ g ; :: thesis: x in L~ f

then consider X being set such that

A116: x in X and

A117: X in { (LSeg (g,i)) where i is Nat : ( 1 <= i & i + 1 <= len g ) } by TARSKI:def 4;

consider i being Nat such that

A118: X = LSeg (g,i) and

A119: 1 <= i and

A120: i + 1 <= len g by A117;

end;assume x in L~ g ; :: thesis: x in L~ f

then consider X being set such that

A116: x in X and

A117: X in { (LSeg (g,i)) where i is Nat : ( 1 <= i & i + 1 <= len g ) } by TARSKI:def 4;

consider i being Nat such that

A118: X = LSeg (g,i) and

A119: 1 <= i and

A120: i + 1 <= len g by A117;

now :: thesis: x in L~ fend;

hence
x in L~ f
; :: thesis: verumper cases
( i + 1 <= len g1 or i + 1 > len g1 )
;

end;

suppose A121:
i + 1 <= len g1
; :: thesis: x in L~ f

i <= i + 1
by NAT_1:11;

then i <= len g1 by A121, XXREAL_0:2;

then A122: i in dom g1 by A119, FINSEQ_3:25;

1 <= i + 1 by NAT_1:11;

then i + 1 in dom g1 by A121, FINSEQ_3:25;

then X = LSeg (g1,i) by A118, A122, TOPREAL3:18;

then X in { (LSeg (g1,j)) where j is Nat : ( 1 <= j & j + 1 <= len g1 ) } by A119, A121;

then A123: x in L~ (f | k) by A36, A116, TARSKI:def 4;

L~ (f | k) c= L~ f by TOPREAL3:20;

hence x in L~ f by A123; :: thesis: verum

end;then i <= len g1 by A121, XXREAL_0:2;

then A122: i in dom g1 by A119, FINSEQ_3:25;

1 <= i + 1 by NAT_1:11;

then i + 1 in dom g1 by A121, FINSEQ_3:25;

then X = LSeg (g1,i) by A118, A122, TOPREAL3:18;

then X in { (LSeg (g1,j)) where j is Nat : ( 1 <= j & j + 1 <= len g1 ) } by A119, A121;

then A123: x in L~ (f | k) by A36, A116, TARSKI:def 4;

L~ (f | k) c= L~ f by TOPREAL3:20;

hence x in L~ f by A123; :: thesis: verum

suppose A124:
i + 1 > len g1
; :: thesis: x in L~ f

reconsider q1 = g /. i, q2 = g /. (i + 1) as Point of (TOP-REAL 2) ;

A125: i <= len g by A120, NAT_1:13;

A126: len g1 <= i by A124, NAT_1:13;

then A127: q1 `1 = (G * (i1,i2)) `1 by A94, A125;

A128: q1 `2 <= (G * (i1,i2)) `2 by A94, A126, A125;

A129: (G * (i1,j2)) `2 <= q1 `2 by A94, A126, A125;

q2 `1 = (G * (i1,i2)) `1 by A94, A120, A124;

then A130: q2 = |[(q1 `1),(q2 `2)]| by A127, EUCLID:53;

A131: q2 `2 <= (G * (i1,i2)) `2 by A94, A120, A124;

A132: ( q1 = |[(q1 `1),(q1 `2)]| & LSeg (g,i) = LSeg (q2,q1) ) by A119, A120, EUCLID:53, TOPREAL1:def 3;

A133: (G * (i1,j2)) `2 <= q2 `2 by A94, A120, A124;

end;A125: i <= len g by A120, NAT_1:13;

A126: len g1 <= i by A124, NAT_1:13;

then A127: q1 `1 = (G * (i1,i2)) `1 by A94, A125;

A128: q1 `2 <= (G * (i1,i2)) `2 by A94, A126, A125;

A129: (G * (i1,j2)) `2 <= q1 `2 by A94, A126, A125;

q2 `1 = (G * (i1,i2)) `1 by A94, A120, A124;

then A130: q2 = |[(q1 `1),(q2 `2)]| by A127, EUCLID:53;

A131: q2 `2 <= (G * (i1,i2)) `2 by A94, A120, A124;

A132: ( q1 = |[(q1 `1),(q1 `2)]| & LSeg (g,i) = LSeg (q2,q1) ) by A119, A120, EUCLID:53, TOPREAL1:def 3;

A133: (G * (i1,j2)) `2 <= q2 `2 by A94, A120, A124;

now :: thesis: x in L~ fend;

hence
x in L~ f
; :: thesis: verumper cases
( q1 `2 > q2 `2 or q1 `2 = q2 `2 or q1 `2 < q2 `2 )
by XXREAL_0:1;

end;

suppose
q1 `2 > q2 `2
; :: thesis: x in L~ f

then
LSeg (g,i) = { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `1 = q1 `1 & q2 `2 <= p2 `2 & p2 `2 <= q1 `2 ) }
by A130, A132, TOPREAL3:9;

then consider p2 being Point of (TOP-REAL 2) such that

A134: ( p2 = x & p2 `1 = q1 `1 ) and

A135: ( q2 `2 <= p2 `2 & p2 `2 <= q1 `2 ) by A116, A118;

( (G * (i1,j2)) `2 <= p2 `2 & p2 `2 <= (G * (i1,i2)) `2 ) by A128, A133, A135, XXREAL_0:2;

then A136: x in LSeg (f,k) by A92, A127, A134;

LSeg (f,k) in { (LSeg (f,j)) where j is Nat : ( 1 <= j & j + 1 <= len f ) } by A3, A13;

hence x in L~ f by A136, TARSKI:def 4; :: thesis: verum

end;then consider p2 being Point of (TOP-REAL 2) such that

A134: ( p2 = x & p2 `1 = q1 `1 ) and

A135: ( q2 `2 <= p2 `2 & p2 `2 <= q1 `2 ) by A116, A118;

( (G * (i1,j2)) `2 <= p2 `2 & p2 `2 <= (G * (i1,i2)) `2 ) by A128, A133, A135, XXREAL_0:2;

then A136: x in LSeg (f,k) by A92, A127, A134;

LSeg (f,k) in { (LSeg (f,j)) where j is Nat : ( 1 <= j & j + 1 <= len f ) } by A3, A13;

hence x in L~ f by A136, TARSKI:def 4; :: thesis: verum

suppose
q1 `2 = q2 `2
; :: thesis: x in L~ f

then
LSeg (g,i) = {q1}
by A130, A132, RLTOPSP1:70;

then x = q1 by A116, A118, TARSKI:def 1;

then A137: x in LSeg (f,k) by A92, A127, A129, A128;

LSeg (f,k) in { (LSeg (f,j)) where j is Nat : ( 1 <= j & j + 1 <= len f ) } by A3, A13;

hence x in L~ f by A137, TARSKI:def 4; :: thesis: verum

end;then x = q1 by A116, A118, TARSKI:def 1;

then A137: x in LSeg (f,k) by A92, A127, A129, A128;

LSeg (f,k) in { (LSeg (f,j)) where j is Nat : ( 1 <= j & j + 1 <= len f ) } by A3, A13;

hence x in L~ f by A137, TARSKI:def 4; :: thesis: verum

suppose
q1 `2 < q2 `2
; :: thesis: x in L~ f

then
LSeg (g,i) = { p1 where p1 is Point of (TOP-REAL 2) : ( p1 `1 = q1 `1 & q1 `2 <= p1 `2 & p1 `2 <= q2 `2 ) }
by A130, A132, TOPREAL3:9;

then consider p2 being Point of (TOP-REAL 2) such that

A138: ( p2 = x & p2 `1 = q1 `1 ) and

A139: ( q1 `2 <= p2 `2 & p2 `2 <= q2 `2 ) by A116, A118;

( (G * (i1,j2)) `2 <= p2 `2 & p2 `2 <= (G * (i1,i2)) `2 ) by A129, A131, A139, XXREAL_0:2;

then A140: x in LSeg (f,k) by A92, A127, A138;

LSeg (f,k) in { (LSeg (f,j)) where j is Nat : ( 1 <= j & j + 1 <= len f ) } by A3, A13;

hence x in L~ f by A140, TARSKI:def 4; :: thesis: verum

end;then consider p2 being Point of (TOP-REAL 2) such that

A138: ( p2 = x & p2 `1 = q1 `1 ) and

A139: ( q1 `2 <= p2 `2 & p2 `2 <= q2 `2 ) by A116, A118;

( (G * (i1,j2)) `2 <= p2 `2 & p2 `2 <= (G * (i1,i2)) `2 ) by A129, A131, A139, XXREAL_0:2;

then A140: x in LSeg (f,k) by A92, A127, A138;

LSeg (f,k) in { (LSeg (f,j)) where j is Nat : ( 1 <= j & j + 1 <= len f ) } by A3, A13;

hence x in L~ f by A140, TARSKI:def 4; :: thesis: verum

assume x in L~ f ; :: thesis: x in L~ g

then A141: x in (L~ (f | k)) \/ (LSeg (f,k)) by A3, A12, Th3;

now :: thesis: x in L~ gend;

hence
x in L~ g
; :: thesis: verumper cases
( x in L~ (f | k) or x in LSeg (f,k) )
by A141, XBOOLE_0:def 3;

end;

suppose
x in LSeg (f,k)
; :: thesis: x in L~ g

then consider p1 being Point of (TOP-REAL 2) such that

A143: p1 = x and

A144: p1 `1 = (G * (i1,i2)) `1 and

A145: (G * (i1,j2)) `2 <= p1 `2 and

A146: p1 `2 <= (G * (i1,i2)) `2 by A92;

defpred S_{3}[ Nat] means ( len g1 <= $1 & $1 <= len g & ( for q being Point of (TOP-REAL 2) st q = g /. $1 holds

q `2 >= p1 `2 ) );

_{3}[n] holds

n <= len g ;

consider ma being Nat such that

A150: ( S_{3}[ma] & ( for n being Nat st S_{3}[n] holds

n <= ma ) ) from NAT_1:sch 6(A149, A147);

reconsider ma = ma as Element of NAT by ORDINAL1:def 12;

end;A143: p1 = x and

A144: p1 `1 = (G * (i1,i2)) `1 and

A145: (G * (i1,j2)) `2 <= p1 `2 and

A146: p1 `2 <= (G * (i1,i2)) `2 by A92;

defpred S

q `2 >= p1 `2 ) );

A147: now :: thesis: ex n being Nat st S_{3}[n]

A149:
for n being Nat st Sreconsider n = len g1 as Nat ;

take n = n; :: thesis: S_{3}[n]

thus S_{3}[n]
:: thesis: verum

end;take n = n; :: thesis: S

thus S

proof

thus
( len g1 <= n & n <= len g )
by A93, XREAL_1:31; :: thesis: for q being Point of (TOP-REAL 2) st q = g /. n holds

q `2 >= p1 `2

1 <= len g1 by A13, A23, A39, XXREAL_0:2;

then A148: len g1 in dom g1 by FINSEQ_3:25;

let q be Point of (TOP-REAL 2); :: thesis: ( q = g /. n implies q `2 >= p1 `2 )

assume q = g /. n ; :: thesis: q `2 >= p1 `2

then q = (f | k) /. (len (f | k)) by A38, A148, FINSEQ_4:68

.= G * (i1,i2) by A17, A23, A14, A19, FINSEQ_4:71 ;

hence q `2 >= p1 `2 by A146; :: thesis: verum

end;q `2 >= p1 `2

1 <= len g1 by A13, A23, A39, XXREAL_0:2;

then A148: len g1 in dom g1 by FINSEQ_3:25;

let q be Point of (TOP-REAL 2); :: thesis: ( q = g /. n implies q `2 >= p1 `2 )

assume q = g /. n ; :: thesis: q `2 >= p1 `2

then q = (f | k) /. (len (f | k)) by A38, A148, FINSEQ_4:68

.= G * (i1,i2) by A17, A23, A14, A19, FINSEQ_4:71 ;

hence q `2 >= p1 `2 by A146; :: thesis: verum

n <= len g ;

consider ma being Nat such that

A150: ( S

n <= ma ) ) from NAT_1:sch 6(A149, A147);

reconsider ma = ma as Element of NAT by ORDINAL1:def 12;

now :: thesis: x in L~ gend;

hence
x in L~ g
; :: thesis: verumper cases
( ma = len g or ma <> len g )
;

end;

suppose A151:
ma = len g
; :: thesis: x in L~ g

j2 + 1 <= i2
by A59, NAT_1:13;

then A152: 1 <= l by XREAL_1:19;

then 0 + 1 <= ma by A73, A93, A151, XREAL_1:7;

then reconsider m1 = ma - 1 as Element of NAT by INT_1:5;

A153: m1 + 1 = ma ;

(len g1) + 1 <= ma by A73, A93, A151, A152, XREAL_1:7;

then A154: m1 >= len g1 by A153, XREAL_1:6;

reconsider q = g /. m1 as Point of (TOP-REAL 2) ;

set lq = { e where e is Point of (TOP-REAL 2) : ( e `1 = (G * (i1,i2)) `1 & (G * (i1,j2)) `2 <= e `2 & e `2 <= q `2 ) } ;

A155: i2 - l = j2 ;

A156: l in dom g2 by A74, A152, FINSEQ_1:1;

then A157: g /. ma = g2 /. l by A73, A93, A151, FINSEQ_4:69

.= G * (i1,j2) by A73, A74, A156, A155 ;

then p1 `2 <= (G * (i1,j2)) `2 by A150;

then A158: p1 `2 = (G * (i1,j2)) `2 by A145, XXREAL_0:1;

A159: m1 <= len g by A151, A153, NAT_1:11;

then A160: q `1 = (G * (i1,i2)) `1 by A94, A154;

A161: (G * (i1,j2)) `2 <= q `2 by A94, A154, A159;

1 <= len g1 by A13, A23, A39, XXREAL_0:2;

then A162: 1 <= m1 by A154, XXREAL_0:2;

then ( q = |[(q `1),(q `2)]| & LSeg (g,m1) = LSeg ((G * (i1,j2)),q) ) by A151, A157, A153, EUCLID:53, TOPREAL1:def 3;

then LSeg (g,m1) = { e where e is Point of (TOP-REAL 2) : ( e `1 = (G * (i1,i2)) `1 & (G * (i1,j2)) `2 <= e `2 & e `2 <= q `2 ) } by A66, A91, A160, A161, TOPREAL3:9;

then A163: p1 in LSeg (g,m1) by A144, A158, A161;

LSeg (g,m1) in { (LSeg (g,i)) where i is Nat : ( 1 <= i & i + 1 <= len g ) } by A151, A153, A162;

hence x in L~ g by A143, A163, TARSKI:def 4; :: thesis: verum

end;then A152: 1 <= l by XREAL_1:19;

then 0 + 1 <= ma by A73, A93, A151, XREAL_1:7;

then reconsider m1 = ma - 1 as Element of NAT by INT_1:5;

A153: m1 + 1 = ma ;

(len g1) + 1 <= ma by A73, A93, A151, A152, XREAL_1:7;

then A154: m1 >= len g1 by A153, XREAL_1:6;

reconsider q = g /. m1 as Point of (TOP-REAL 2) ;

set lq = { e where e is Point of (TOP-REAL 2) : ( e `1 = (G * (i1,i2)) `1 & (G * (i1,j2)) `2 <= e `2 & e `2 <= q `2 ) } ;

A155: i2 - l = j2 ;

A156: l in dom g2 by A74, A152, FINSEQ_1:1;

then A157: g /. ma = g2 /. l by A73, A93, A151, FINSEQ_4:69

.= G * (i1,j2) by A73, A74, A156, A155 ;

then p1 `2 <= (G * (i1,j2)) `2 by A150;

then A158: p1 `2 = (G * (i1,j2)) `2 by A145, XXREAL_0:1;

A159: m1 <= len g by A151, A153, NAT_1:11;

then A160: q `1 = (G * (i1,i2)) `1 by A94, A154;

A161: (G * (i1,j2)) `2 <= q `2 by A94, A154, A159;

1 <= len g1 by A13, A23, A39, XXREAL_0:2;

then A162: 1 <= m1 by A154, XXREAL_0:2;

then ( q = |[(q `1),(q `2)]| & LSeg (g,m1) = LSeg ((G * (i1,j2)),q) ) by A151, A157, A153, EUCLID:53, TOPREAL1:def 3;

then LSeg (g,m1) = { e where e is Point of (TOP-REAL 2) : ( e `1 = (G * (i1,i2)) `1 & (G * (i1,j2)) `2 <= e `2 & e `2 <= q `2 ) } by A66, A91, A160, A161, TOPREAL3:9;

then A163: p1 in LSeg (g,m1) by A144, A158, A161;

LSeg (g,m1) in { (LSeg (g,i)) where i is Nat : ( 1 <= i & i + 1 <= len g ) } by A151, A153, A162;

hence x in L~ g by A143, A163, TARSKI:def 4; :: thesis: verum

suppose
ma <> len g
; :: thesis: x in L~ g

then
ma < len g
by A150, XXREAL_0:1;

then A164: ma + 1 <= len g by NAT_1:13;

reconsider qa = g /. ma, qa1 = g /. (ma + 1) as Point of (TOP-REAL 2) ;

set lma = { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `1 = (G * (i1,i2)) `1 & qa1 `2 <= p2 `2 & p2 `2 <= qa `2 ) } ;

A165: qa1 = |[(qa1 `1),(qa1 `2)]| by EUCLID:53;

A166: p1 `2 <= qa `2 by A150;

A167: len g1 <= ma + 1 by A150, NAT_1:13;

then A168: qa1 `1 = (G * (i1,i2)) `1 by A94, A164;

A171: 1 <= ma by A13, A23, A39, A150, NAT_1:13;

then LSeg (g,ma) = LSeg (qa1,qa) by A164, TOPREAL1:def 3

.= { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `1 = (G * (i1,i2)) `1 & qa1 `2 <= p2 `2 & p2 `2 <= qa `2 ) } by A166, A169, A168, A170, A165, TOPREAL3:9, XXREAL_0:2 ;

then A172: x in LSeg (g,ma) by A143, A144, A166, A169;

LSeg (g,ma) in { (LSeg (g,i)) where i is Nat : ( 1 <= i & i + 1 <= len g ) } by A171, A164;

hence x in L~ g by A172, TARSKI:def 4; :: thesis: verum

end;then A164: ma + 1 <= len g by NAT_1:13;

reconsider qa = g /. ma, qa1 = g /. (ma + 1) as Point of (TOP-REAL 2) ;

set lma = { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `1 = (G * (i1,i2)) `1 & qa1 `2 <= p2 `2 & p2 `2 <= qa `2 ) } ;

A165: qa1 = |[(qa1 `1),(qa1 `2)]| by EUCLID:53;

A166: p1 `2 <= qa `2 by A150;

A167: len g1 <= ma + 1 by A150, NAT_1:13;

then A168: qa1 `1 = (G * (i1,i2)) `1 by A94, A164;

A169: now :: thesis: not p1 `2 <= qa1 `2

A170:
( qa `1 = (G * (i1,i2)) `1 & qa = |[(qa `1),(qa `2)]| )
by A94, A150, EUCLID:53;assume
p1 `2 <= qa1 `2
; :: thesis: contradiction

then for q being Point of (TOP-REAL 2) st q = g /. (ma + 1) holds

p1 `2 <= q `2 ;

then ma + 1 <= ma by A150, A164, A167;

hence contradiction by XREAL_1:29; :: thesis: verum

end;then for q being Point of (TOP-REAL 2) st q = g /. (ma + 1) holds

p1 `2 <= q `2 ;

then ma + 1 <= ma by A150, A164, A167;

hence contradiction by XREAL_1:29; :: thesis: verum

A171: 1 <= ma by A13, A23, A39, A150, NAT_1:13;

then LSeg (g,ma) = LSeg (qa1,qa) by A164, TOPREAL1:def 3

.= { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `1 = (G * (i1,i2)) `1 & qa1 `2 <= p2 `2 & p2 `2 <= qa `2 ) } by A166, A169, A168, A170, A165, TOPREAL3:9, XXREAL_0:2 ;

then A172: x in LSeg (g,ma) by A143, A144, A166, A169;

LSeg (g,ma) in { (LSeg (g,i)) where i is Nat : ( 1 <= i & i + 1 <= len g ) } by A171, A164;

hence x in L~ g by A172, TARSKI:def 4; :: thesis: verum

then 1 in dom g1 by FINSEQ_3:25;

hence g /. 1 = (f | k) /. 1 by A37, FINSEQ_4:68

.= f /. 1 by A17, A15, FINSEQ_4:71 ;

:: thesis: ( g /. (len g) = f /. (len f) & len f <= len g )

A173: len g = (len g1) + (len g2) by FINSEQ_1:22;

j2 + 1 <= i2 by A59, NAT_1:13;

then A174: 1 <= l by XREAL_1:19;

then A175: l in dom g2 by A74, FINSEQ_1:1;

hence g /. (len g) = g2 /. l by A73, A173, FINSEQ_4:69

.= G * (i1,m1) by A73, A74, A175

.= f /. (len f) by A3, A46, A58 ;

:: thesis: len f <= len g

thus len f <= len g by A3, A23, A39, A73, A174, A173, XREAL_1:7; :: thesis: verum

case A176:
i2 < j2
; :: thesis: ex g being FinSequence of the carrier of (TOP-REAL 2) st

( g is_sequence_on G & L~ g = L~ f & g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g )

( g is_sequence_on G & L~ g = L~ f & g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g )

set lk = { w where w is Point of (TOP-REAL 2) : ( w `1 = (G * (i1,i2)) `1 & (G * (i1,i2)) `2 <= w `2 & w `2 <= (G * (i1,j2)) `2 ) } ;

A177: G * (i1,i2) = |[((G * (i1,i2)) `1),((G * (i1,i2)) `2)]| by EUCLID:53;

reconsider l = j2 - i2 as Element of NAT by A176, INT_1:5;

deffunc H_{1}( Nat) -> Element of the carrier of (TOP-REAL 2) = G * (i1,(i2 + $1));

consider g2 being FinSequence of (TOP-REAL 2) such that

A178: ( len g2 = l & ( for n being Nat st n in dom g2 holds

g2 /. n = H_{1}(n) ) )
from FINSEQ_4:sch 2();

take g = g1 ^ g2; :: thesis: ( g is_sequence_on G & L~ g = L~ f & g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g )

ex i, j being Nat st

( [i,j] in Indices G & g /. n = G * (i,j) ) by A40, GOBOARD1:23;

for m, k, i, j being Nat st [m,k] in Indices G & [i,j] in Indices G & g /. n = G * (m,k) & g /. (n + 1) = G * (i,j) holds

|.(m - i).| + |.(k - j).| = 1 by A41, A187, GOBOARD1:24;

hence g is_sequence_on G by A186; :: thesis: ( L~ g = L~ f & g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g )

A201: G * (i1,j2) = |[((G * (i1,j2)) `1),((G * (i1,j2)) `2)]| by EUCLID:53;

j2 in dom l1 by A56, A55, FINSEQ_1:def 3;

then l1 /. j2 = l1 . j2 by PARTFUN1:def 6;

then A202: l1 /. j2 = G * (i1,j2) by A56, MATRIX_0:def 7;

then A203: (Y_axis l1) . j2 = (G * (i1,j2)) `2 by A56, A20, A55, GOBOARD1:def 2;

i2 in dom l1 by A51, A55, FINSEQ_1:def 3;

then l1 /. i2 = l1 . i2 by PARTFUN1:def 6;

then A204: l1 /. i2 = G * (i1,i2) by A51, MATRIX_0:def 7;

then A205: (Y_axis l1) . i2 = (G * (i1,i2)) `2 by A51, A20, A55, GOBOARD1:def 2;

then A206: (G * (i1,i2)) `2 < (G * (i1,j2)) `2 by A51, A56, A54, A20, A55, A176, A203, SEQM_3:def 1;

A207: (X_axis l1) . j2 = (G * (i1,j2)) `1 by A56, A42, A55, A202, GOBOARD1:def 1;

(X_axis l1) . i2 = (G * (i1,i2)) `1 by A51, A42, A55, A204, GOBOARD1:def 1;

then A208: (G * (i1,i2)) `1 = (G * (i1,j2)) `1 by A51, A56, A50, A42, A55, A207, SEQM_3:def 10;

A209: LSeg (f,k) = LSeg ((G * (i1,i2)),(G * (i1,j2))) by A3, A13, A19, A46, A58, TOPREAL1:def 3

.= { w where w is Point of (TOP-REAL 2) : ( w `1 = (G * (i1,i2)) `1 & (G * (i1,i2)) `2 <= w `2 & w `2 <= (G * (i1,j2)) `2 ) } by A206, A208, A177, A201, TOPREAL3:9 ;

A210: dom g2 = Seg l by A178, FINSEQ_1:def 3;

thus L~ g = L~ f :: thesis: ( g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g )

then 1 in dom g1 by FINSEQ_3:25;

hence g /. 1 = (f | k) /. 1 by A37, FINSEQ_4:68

.= f /. 1 by A17, A15, FINSEQ_4:71 ;

:: thesis: ( g /. (len g) = f /. (len f) & len f <= len g )

A291: len g = (len g1) + l by A178, FINSEQ_1:22;

i2 + 1 <= j2 by A176, NAT_1:13;

then A292: 1 <= l by XREAL_1:19;

then A293: l in dom g2 by A178, A184, FINSEQ_1:1;

hence g /. (len g) = g2 /. l by A291, FINSEQ_4:69

.= G * (i1,(i2 + l)) by A178, A293

.= f /. (len f) by A3, A46, A58 ;

:: thesis: len f <= len g

thus len f <= len g by A3, A23, A39, A292, A291, XREAL_1:7; :: thesis: verum

end;A177: G * (i1,i2) = |[((G * (i1,i2)) `1),((G * (i1,i2)) `2)]| by EUCLID:53;

reconsider l = j2 - i2 as Element of NAT by A176, INT_1:5;

deffunc H

consider g2 being FinSequence of (TOP-REAL 2) such that

A178: ( len g2 = l & ( for n being Nat st n in dom g2 holds

g2 /. n = H

take g = g1 ^ g2; :: thesis: ( g is_sequence_on G & L~ g = L~ f & g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g )

A179: now :: thesis: for n being Nat st n in Seg l holds

( i2 + n in Seg (width G) & [i1,(i2 + n)] in Indices G )

A184:
dom g2 = Seg (len g2)
by FINSEQ_1:def 3;( i2 + n in Seg (width G) & [i1,(i2 + n)] in Indices G )

let n be Nat; :: thesis: ( n in Seg l implies ( i2 + n in Seg (width G) & [i1,(i2 + n)] in Indices G ) )

A180: n <= i2 + n by NAT_1:11;

assume A181: n in Seg l ; :: thesis: ( i2 + n in Seg (width G) & [i1,(i2 + n)] in Indices G )

then n <= l by FINSEQ_1:1;

then A182: i2 + n <= l + i2 by XREAL_1:7;

j2 <= width G by A56, FINSEQ_1:1;

then A183: i2 + n <= width G by A182, XXREAL_0:2;

1 <= n by A181, FINSEQ_1:1;

then 1 <= i2 + n by A180, XXREAL_0:2;

hence i2 + n in Seg (width G) by A183, FINSEQ_1:1; :: thesis: [i1,(i2 + n)] in Indices G

hence [i1,(i2 + n)] in Indices G by A47, A49, ZFMISC_1:87; :: thesis: verum

end;A180: n <= i2 + n by NAT_1:11;

assume A181: n in Seg l ; :: thesis: ( i2 + n in Seg (width G) & [i1,(i2 + n)] in Indices G )

then n <= l by FINSEQ_1:1;

then A182: i2 + n <= l + i2 by XREAL_1:7;

j2 <= width G by A56, FINSEQ_1:1;

then A183: i2 + n <= width G by A182, XXREAL_0:2;

1 <= n by A181, FINSEQ_1:1;

then 1 <= i2 + n by A180, XXREAL_0:2;

hence i2 + n in Seg (width G) by A183, FINSEQ_1:1; :: thesis: [i1,(i2 + n)] in Indices G

hence [i1,(i2 + n)] in Indices G by A47, A49, ZFMISC_1:87; :: thesis: verum

now :: thesis: for n being Nat st n in dom g2 holds

ex m being Nat ex k being set st

( [m,k] in Indices G & g2 /. n = G * (m,k) )

then A186:
for n being Nat st n in dom g holds ex m being Nat ex k being set st

( [m,k] in Indices G & g2 /. n = G * (m,k) )

let n be Nat; :: thesis: ( n in dom g2 implies ex m being Nat ex k being set st

( [m,k] in Indices G & g2 /. n = G * (m,k) ) )

assume A185: n in dom g2 ; :: thesis: ex m being Nat ex k being set st

( [m,k] in Indices G & g2 /. n = G * (m,k) )

take m = i1; :: thesis: ex k being set st

( [m,k] in Indices G & g2 /. n = G * (m,k) )

take k = i2 + n; :: thesis: ( [m,k] in Indices G & g2 /. n = G * (m,k) )

thus ( [m,k] in Indices G & g2 /. n = G * (m,k) ) by A178, A179, A184, A185; :: thesis: verum

end;( [m,k] in Indices G & g2 /. n = G * (m,k) ) )

assume A185: n in dom g2 ; :: thesis: ex m being Nat ex k being set st

( [m,k] in Indices G & g2 /. n = G * (m,k) )

take m = i1; :: thesis: ex k being set st

( [m,k] in Indices G & g2 /. n = G * (m,k) )

take k = i2 + n; :: thesis: ( [m,k] in Indices G & g2 /. n = G * (m,k) )

thus ( [m,k] in Indices G & g2 /. n = G * (m,k) ) by A178, A179, A184, A185; :: thesis: verum

ex i, j being Nat st

( [i,j] in Indices G & g /. n = G * (i,j) ) by A40, GOBOARD1:23;

A187: now :: thesis: for n being Nat st n in dom g2 & n + 1 in dom g2 holds

for l1, l2, l3, l4 being Nat st [l1,l2] in Indices G & [l3,l4] in Indices G & g2 /. n = G * (l1,l2) & g2 /. (n + 1) = G * (l3,l4) holds

|.(l1 - l3).| + |.(l2 - l4).| = 1

for l1, l2, l3, l4 being Nat st [l1,l2] in Indices G & [l3,l4] in Indices G & g2 /. n = G * (l1,l2) & g2 /. (n + 1) = G * (l3,l4) holds

|.(l1 - l3).| + |.(l2 - l4).| = 1

let n be Nat; :: thesis: ( n in dom g2 & n + 1 in dom g2 implies for l1, l2, l3, l4 being Nat st [l1,l2] in Indices G & [l3,l4] in Indices G & g2 /. n = G * (l1,l2) & g2 /. (n + 1) = G * (l3,l4) holds

|.(l1 - l3).| + |.(l2 - l4).| = 1 )

assume that

A188: n in dom g2 and

A189: n + 1 in dom g2 ; :: thesis: for l1, l2, l3, l4 being Nat st [l1,l2] in Indices G & [l3,l4] in Indices G & g2 /. n = G * (l1,l2) & g2 /. (n + 1) = G * (l3,l4) holds

|.(l1 - l3).| + |.(l2 - l4).| = 1

let l1, l2, l3, l4 be Nat; :: thesis: ( [l1,l2] in Indices G & [l3,l4] in Indices G & g2 /. n = G * (l1,l2) & g2 /. (n + 1) = G * (l3,l4) implies |.(l1 - l3).| + |.(l2 - l4).| = 1 )

assume that

A190: [l1,l2] in Indices G and

A191: [l3,l4] in Indices G and

A192: g2 /. n = G * (l1,l2) and

A193: g2 /. (n + 1) = G * (l3,l4) ; :: thesis: |.(l1 - l3).| + |.(l2 - l4).| = 1

( g2 /. (n + 1) = G * (i1,(i2 + (n + 1))) & [i1,(i2 + (n + 1))] in Indices G ) by A178, A179, A184, A189;

then A194: ( l3 = i1 & l4 = i2 + (n + 1) ) by A191, A193, GOBOARD1:5;

( g2 /. n = G * (i1,(i2 + n)) & [i1,(i2 + n)] in Indices G ) by A178, A179, A184, A188;

then ( l1 = i1 & l2 = i2 + n ) by A190, A192, GOBOARD1:5;

hence |.(l1 - l3).| + |.(l2 - l4).| = 0 + |.((i2 + n) - (i2 + (n + 1))).| by A194, ABSVALUE:2

.= |.(- 1).|

.= |.1.| by COMPLEX1:52

.= 1 by ABSVALUE:def 1 ;

:: thesis: verum

end;|.(l1 - l3).| + |.(l2 - l4).| = 1 )

assume that

A188: n in dom g2 and

A189: n + 1 in dom g2 ; :: thesis: for l1, l2, l3, l4 being Nat st [l1,l2] in Indices G & [l3,l4] in Indices G & g2 /. n = G * (l1,l2) & g2 /. (n + 1) = G * (l3,l4) holds

|.(l1 - l3).| + |.(l2 - l4).| = 1

let l1, l2, l3, l4 be Nat; :: thesis: ( [l1,l2] in Indices G & [l3,l4] in Indices G & g2 /. n = G * (l1,l2) & g2 /. (n + 1) = G * (l3,l4) implies |.(l1 - l3).| + |.(l2 - l4).| = 1 )

assume that

A190: [l1,l2] in Indices G and

A191: [l3,l4] in Indices G and

A192: g2 /. n = G * (l1,l2) and

A193: g2 /. (n + 1) = G * (l3,l4) ; :: thesis: |.(l1 - l3).| + |.(l2 - l4).| = 1

( g2 /. (n + 1) = G * (i1,(i2 + (n + 1))) & [i1,(i2 + (n + 1))] in Indices G ) by A178, A179, A184, A189;

then A194: ( l3 = i1 & l4 = i2 + (n + 1) ) by A191, A193, GOBOARD1:5;

( g2 /. n = G * (i1,(i2 + n)) & [i1,(i2 + n)] in Indices G ) by A178, A179, A184, A188;

then ( l1 = i1 & l2 = i2 + n ) by A190, A192, GOBOARD1:5;

hence |.(l1 - l3).| + |.(l2 - l4).| = 0 + |.((i2 + n) - (i2 + (n + 1))).| by A194, ABSVALUE:2

.= |.(- 1).|

.= |.1.| by COMPLEX1:52

.= 1 by ABSVALUE:def 1 ;

:: thesis: verum

now :: thesis: for l1, l2, l3, l4 being Nat st [l1,l2] in Indices G & [l3,l4] in Indices G & g1 /. (len g1) = G * (l1,l2) & g2 /. 1 = G * (l3,l4) & len g1 in dom g1 & 1 in dom g2 holds

|.(l1 - l3).| + |.(l2 - l4).| = 1

then
for n being Nat st n in dom g & n + 1 in dom g holds |.(l1 - l3).| + |.(l2 - l4).| = 1

let l1, l2, l3, l4 be Nat; :: thesis: ( [l1,l2] in Indices G & [l3,l4] in Indices G & g1 /. (len g1) = G * (l1,l2) & g2 /. 1 = G * (l3,l4) & len g1 in dom g1 & 1 in dom g2 implies |.(l1 - l3).| + |.(l2 - l4).| = 1 )

assume that

A195: [l1,l2] in Indices G and

A196: [l3,l4] in Indices G and

A197: g1 /. (len g1) = G * (l1,l2) and

A198: g2 /. 1 = G * (l3,l4) and

len g1 in dom g1 and

A199: 1 in dom g2 ; :: thesis: |.(l1 - l3).| + |.(l2 - l4).| = 1

( g2 /. 1 = G * (i1,(i2 + 1)) & [i1,(i2 + 1)] in Indices G ) by A178, A179, A184, A199;

then A200: ( l3 = i1 & l4 = i2 + 1 ) by A196, A198, GOBOARD1:5;

(f | k) /. (len (f | k)) = f /. k by A17, A23, A14, FINSEQ_4:71;

then ( l1 = i1 & l2 = i2 ) by A38, A18, A19, A195, A197, GOBOARD1:5;

hence |.(l1 - l3).| + |.(l2 - l4).| = 0 + |.(i2 - (i2 + 1)).| by A200, ABSVALUE:2

.= |.((i2 - i2) + (- 1)).|

.= |.1.| by COMPLEX1:52

.= 1 by ABSVALUE:def 1 ;

:: thesis: verum

end;assume that

A195: [l1,l2] in Indices G and

A196: [l3,l4] in Indices G and

A197: g1 /. (len g1) = G * (l1,l2) and

A198: g2 /. 1 = G * (l3,l4) and

len g1 in dom g1 and

A199: 1 in dom g2 ; :: thesis: |.(l1 - l3).| + |.(l2 - l4).| = 1

( g2 /. 1 = G * (i1,(i2 + 1)) & [i1,(i2 + 1)] in Indices G ) by A178, A179, A184, A199;

then A200: ( l3 = i1 & l4 = i2 + 1 ) by A196, A198, GOBOARD1:5;

(f | k) /. (len (f | k)) = f /. k by A17, A23, A14, FINSEQ_4:71;

then ( l1 = i1 & l2 = i2 ) by A38, A18, A19, A195, A197, GOBOARD1:5;

hence |.(l1 - l3).| + |.(l2 - l4).| = 0 + |.(i2 - (i2 + 1)).| by A200, ABSVALUE:2

.= |.((i2 - i2) + (- 1)).|

.= |.1.| by COMPLEX1:52

.= 1 by ABSVALUE:def 1 ;

:: thesis: verum

for m, k, i, j being Nat st [m,k] in Indices G & [i,j] in Indices G & g /. n = G * (m,k) & g /. (n + 1) = G * (i,j) holds

|.(m - i).| + |.(k - j).| = 1 by A41, A187, GOBOARD1:24;

hence g is_sequence_on G by A186; :: thesis: ( L~ g = L~ f & g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g )

A201: G * (i1,j2) = |[((G * (i1,j2)) `1),((G * (i1,j2)) `2)]| by EUCLID:53;

j2 in dom l1 by A56, A55, FINSEQ_1:def 3;

then l1 /. j2 = l1 . j2 by PARTFUN1:def 6;

then A202: l1 /. j2 = G * (i1,j2) by A56, MATRIX_0:def 7;

then A203: (Y_axis l1) . j2 = (G * (i1,j2)) `2 by A56, A20, A55, GOBOARD1:def 2;

i2 in dom l1 by A51, A55, FINSEQ_1:def 3;

then l1 /. i2 = l1 . i2 by PARTFUN1:def 6;

then A204: l1 /. i2 = G * (i1,i2) by A51, MATRIX_0:def 7;

then A205: (Y_axis l1) . i2 = (G * (i1,i2)) `2 by A51, A20, A55, GOBOARD1:def 2;

then A206: (G * (i1,i2)) `2 < (G * (i1,j2)) `2 by A51, A56, A54, A20, A55, A176, A203, SEQM_3:def 1;

A207: (X_axis l1) . j2 = (G * (i1,j2)) `1 by A56, A42, A55, A202, GOBOARD1:def 1;

(X_axis l1) . i2 = (G * (i1,i2)) `1 by A51, A42, A55, A204, GOBOARD1:def 1;

then A208: (G * (i1,i2)) `1 = (G * (i1,j2)) `1 by A51, A56, A50, A42, A55, A207, SEQM_3:def 10;

A209: LSeg (f,k) = LSeg ((G * (i1,i2)),(G * (i1,j2))) by A3, A13, A19, A46, A58, TOPREAL1:def 3

.= { w where w is Point of (TOP-REAL 2) : ( w `1 = (G * (i1,i2)) `1 & (G * (i1,i2)) `2 <= w `2 & w `2 <= (G * (i1,j2)) `2 ) } by A206, A208, A177, A201, TOPREAL3:9 ;

A210: dom g2 = Seg l by A178, FINSEQ_1:def 3;

thus L~ g = L~ f :: thesis: ( g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g )

proof

1 <= len g1
by A13, A23, A39, XXREAL_0:2;
set lg = { (LSeg (g,i)) where i is Nat : ( 1 <= i & i + 1 <= len g ) } ;

set lf = { (LSeg (f,j)) where j is Nat : ( 1 <= j & j + 1 <= len f ) } ;

A211: len g = (len g1) + (len g2) by FINSEQ_1:22;

assume x in L~ f ; :: thesis: x in L~ g

then A259: x in (L~ (f | k)) \/ (LSeg (f,k)) by A3, A12, Th3;

end;set lf = { (LSeg (f,j)) where j is Nat : ( 1 <= j & j + 1 <= len f ) } ;

A211: len g = (len g1) + (len g2) by FINSEQ_1:22;

A212: now :: thesis: for j being Nat st len g1 <= j & j <= len g holds

for p being Point of (TOP-REAL 2) st p = g /. j holds

( p `1 = (G * (i1,i2)) `1 & (G * (i1,i2)) `2 <= p `2 & p `2 <= (G * (i1,j2)) `2 & p in rng l1 )

thus
L~ g c= L~ f
:: according to XBOOLE_0:def 10 :: thesis: L~ f c= L~ gfor p being Point of (TOP-REAL 2) st p = g /. j holds

( p `1 = (G * (i1,i2)) `1 & (G * (i1,i2)) `2 <= p `2 & p `2 <= (G * (i1,j2)) `2 & p in rng l1 )

let j be Nat; :: thesis: ( len g1 <= j & j <= len g implies for p being Point of (TOP-REAL 2) st p = g /. j holds

( p `1 = (G * (i1,i2)) `1 & (G * (i1,i2)) `2 <= p `2 & p `2 <= (G * (i1,j2)) `2 & p in rng l1 ) )

assume that

A213: len g1 <= j and

A214: j <= len g ; :: thesis: for p being Point of (TOP-REAL 2) st p = g /. j holds

( p `1 = (G * (i1,i2)) `1 & (G * (i1,i2)) `2 <= p `2 & p `2 <= (G * (i1,j2)) `2 & p in rng l1 )

reconsider w = j - (len g1) as Element of NAT by A213, INT_1:5;

let p be Point of (TOP-REAL 2); :: thesis: ( p = g /. j implies ( p `1 = (G * (i1,i2)) `1 & (G * (i1,i2)) `2 <= p `2 & p `2 <= (G * (i1,j2)) `2 & p in rng l1 ) )

assume A215: p = g /. j ; :: thesis: ( p `1 = (G * (i1,i2)) `1 & (G * (i1,i2)) `2 <= p `2 & p `2 <= (G * (i1,j2)) `2 & p in rng l1 )

set u = i2 + w;

A216: dom l1 = Seg (len l1) by FINSEQ_1:def 3;

end;( p `1 = (G * (i1,i2)) `1 & (G * (i1,i2)) `2 <= p `2 & p `2 <= (G * (i1,j2)) `2 & p in rng l1 ) )

assume that

A213: len g1 <= j and

A214: j <= len g ; :: thesis: for p being Point of (TOP-REAL 2) st p = g /. j holds

( p `1 = (G * (i1,i2)) `1 & (G * (i1,i2)) `2 <= p `2 & p `2 <= (G * (i1,j2)) `2 & p in rng l1 )

reconsider w = j - (len g1) as Element of NAT by A213, INT_1:5;

let p be Point of (TOP-REAL 2); :: thesis: ( p = g /. j implies ( p `1 = (G * (i1,i2)) `1 & (G * (i1,i2)) `2 <= p `2 & p `2 <= (G * (i1,j2)) `2 & p in rng l1 ) )

assume A215: p = g /. j ; :: thesis: ( p `1 = (G * (i1,i2)) `1 & (G * (i1,i2)) `2 <= p `2 & p `2 <= (G * (i1,j2)) `2 & p in rng l1 )

set u = i2 + w;

A216: dom l1 = Seg (len l1) by FINSEQ_1:def 3;

now :: thesis: ( p `1 = (G * (i1,i2)) `1 & (G * (i1,i2)) `2 <= p `2 & p `2 <= (G * (i1,j2)) `2 & p in rng l1 )end;

hence
( p `1 = (G * (i1,i2)) `1 & (G * (i1,i2)) `2 <= p `2 & p `2 <= (G * (i1,j2)) `2 & p in rng l1 )
; :: thesis: verumper cases
( j = len g1 or j <> len g1 )
;

end;

suppose A217:
j = len g1
; :: thesis: ( p `1 = (G * (i1,i2)) `1 & (G * (i1,i2)) `2 <= p `2 & p `2 <= (G * (i1,j2)) `2 & p in rng l1 )

1 <= len g1
by A13, A23, A39, XXREAL_0:2;

then len g1 in dom g1 by FINSEQ_3:25;

then A218: g /. (len g1) = (f | k) /. (len (f | k)) by A38, FINSEQ_4:68

.= G * (i1,i2) by A17, A23, A14, A19, FINSEQ_4:71 ;

hence p `1 = (G * (i1,i2)) `1 by A215, A217; :: thesis: ( (G * (i1,i2)) `2 <= p `2 & p `2 <= (G * (i1,j2)) `2 & p in rng l1 )

thus ( (G * (i1,i2)) `2 <= p `2 & p `2 <= (G * (i1,j2)) `2 ) by A51, A56, A54, A20, A55, A176, A205, A203, A215, A217, A218, SEQM_3:def 1; :: thesis: p in rng l1

thus p in rng l1 by A51, A55, A204, A215, A216, A217, A218, PARTFUN2:2; :: thesis: verum

end;then len g1 in dom g1 by FINSEQ_3:25;

then A218: g /. (len g1) = (f | k) /. (len (f | k)) by A38, FINSEQ_4:68

.= G * (i1,i2) by A17, A23, A14, A19, FINSEQ_4:71 ;

hence p `1 = (G * (i1,i2)) `1 by A215, A217; :: thesis: ( (G * (i1,i2)) `2 <= p `2 & p `2 <= (G * (i1,j2)) `2 & p in rng l1 )

thus ( (G * (i1,i2)) `2 <= p `2 & p `2 <= (G * (i1,j2)) `2 ) by A51, A56, A54, A20, A55, A176, A205, A203, A215, A217, A218, SEQM_3:def 1; :: thesis: p in rng l1

thus p in rng l1 by A51, A55, A204, A215, A216, A217, A218, PARTFUN2:2; :: thesis: verum

suppose A219:
j <> len g1
; :: thesis: ( p `1 = (G * (i1,i2)) `1 & (G * (i1,i2)) `2 <= p `2 & p `2 <= (G * (i1,j2)) `2 & p in rng l1 )

A220:
w + (len g1) = j
;

then A221: w <= len g2 by A211, A214, XREAL_1:6;

A222: (X_axis l1) . i2 = (G * (i1,i2)) `1 by A51, A42, A55, A204, GOBOARD1:def 1;

A223: j - (len g1) <> 0 by A219;

then A224: w >= 1 by NAT_1:14;

then A225: g /. j = g2 /. w by A220, A221, SEQ_4:136;

A226: i2 < i2 + w by A223, XREAL_1:29;

A227: w in dom g2 by A224, A221, FINSEQ_3:25;

then A228: i2 + w in Seg (width G) by A210, A179;

i2 + w in Seg (width G) by A210, A179, A227;

then i2 + w in dom l1 by A55, FINSEQ_1:def 3;

then l1 /. (i2 + w) = l1 . (i2 + w) by PARTFUN1:def 6;

then A229: l1 /. (i2 + w) = G * (i1,(i2 + w)) by A228, MATRIX_0:def 7;

then A230: (Y_axis l1) . (i2 + w) = (G * (i1,(i2 + w))) `2 by A20, A55, A228, GOBOARD1:def 2;

A231: g2 /. w = G * (i1,(i2 + w)) by A178, A227;

(X_axis l1) . (i2 + w) = (G * (i1,(i2 + w))) `1 by A42, A55, A228, A229, GOBOARD1:def 1;

hence p `1 = (G * (i1,i2)) `1 by A51, A50, A42, A55, A215, A225, A231, A228, A222, SEQM_3:def 10; :: thesis: ( (G * (i1,i2)) `2 <= p `2 & p `2 <= (G * (i1,j2)) `2 & p in rng l1 )

(Y_axis l1) . i2 = (G * (i1,i2)) `2 by A51, A20, A55, A204, GOBOARD1:def 2;

hence (G * (i1,i2)) `2 <= p `2 by A51, A54, A20, A55, A215, A225, A231, A228, A230, A226, SEQM_3:def 1; :: thesis: ( p `2 <= (G * (i1,j2)) `2 & p in rng l1 )

A232: (Y_axis l1) . j2 = (G * (i1,j2)) `2 by A56, A20, A55, A202, GOBOARD1:def 2;

thus p in rng l1 by A55, A215, A216, A225, A231, A228, A229, PARTFUN2:2; :: thesis: verum

end;then A221: w <= len g2 by A211, A214, XREAL_1:6;

A222: (X_axis l1) . i2 = (G * (i1,i2)) `1 by A51, A42, A55, A204, GOBOARD1:def 1;

A223: j - (len g1) <> 0 by A219;

then A224: w >= 1 by NAT_1:14;

then A225: g /. j = g2 /. w by A220, A221, SEQ_4:136;

A226: i2 < i2 + w by A223, XREAL_1:29;

A227: w in dom g2 by A224, A221, FINSEQ_3:25;

then A228: i2 + w in Seg (width G) by A210, A179;

i2 + w in Seg (width G) by A210, A179, A227;

then i2 + w in dom l1 by A55, FINSEQ_1:def 3;

then l1 /. (i2 + w) = l1 . (i2 + w) by PARTFUN1:def 6;

then A229: l1 /. (i2 + w) = G * (i1,(i2 + w)) by A228, MATRIX_0:def 7;

then A230: (Y_axis l1) . (i2 + w) = (G * (i1,(i2 + w))) `2 by A20, A55, A228, GOBOARD1:def 2;

A231: g2 /. w = G * (i1,(i2 + w)) by A178, A227;

(X_axis l1) . (i2 + w) = (G * (i1,(i2 + w))) `1 by A42, A55, A228, A229, GOBOARD1:def 1;

hence p `1 = (G * (i1,i2)) `1 by A51, A50, A42, A55, A215, A225, A231, A228, A222, SEQM_3:def 10; :: thesis: ( (G * (i1,i2)) `2 <= p `2 & p `2 <= (G * (i1,j2)) `2 & p in rng l1 )

(Y_axis l1) . i2 = (G * (i1,i2)) `2 by A51, A20, A55, A204, GOBOARD1:def 2;

hence (G * (i1,i2)) `2 <= p `2 by A51, A54, A20, A55, A215, A225, A231, A228, A230, A226, SEQM_3:def 1; :: thesis: ( p `2 <= (G * (i1,j2)) `2 & p in rng l1 )

A232: (Y_axis l1) . j2 = (G * (i1,j2)) `2 by A56, A20, A55, A202, GOBOARD1:def 2;

now :: thesis: p `2 <= (G * (i1,j2)) `2

hence
p `2 <= (G * (i1,j2)) `2
; :: thesis: p in rng l1end;

thus p in rng l1 by A55, A215, A216, A225, A231, A228, A229, PARTFUN2:2; :: thesis: verum

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in L~ f or x in L~ g )
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in L~ g or x in L~ f )

assume x in L~ g ; :: thesis: x in L~ f

then consider X being set such that

A234: x in X and

A235: X in { (LSeg (g,i)) where i is Nat : ( 1 <= i & i + 1 <= len g ) } by TARSKI:def 4;

consider i being Nat such that

A236: X = LSeg (g,i) and

A237: 1 <= i and

A238: i + 1 <= len g by A235;

end;assume x in L~ g ; :: thesis: x in L~ f

then consider X being set such that

A234: x in X and

A235: X in { (LSeg (g,i)) where i is Nat : ( 1 <= i & i + 1 <= len g ) } by TARSKI:def 4;

consider i being Nat such that

A236: X = LSeg (g,i) and

A237: 1 <= i and

A238: i + 1 <= len g by A235;

now :: thesis: x in L~ fend;

hence
x in L~ f
; :: thesis: verumper cases
( i + 1 <= len g1 or i + 1 > len g1 )
;

end;

suppose A239:
i + 1 <= len g1
; :: thesis: x in L~ f

i <= i + 1
by NAT_1:11;

then i <= len g1 by A239, XXREAL_0:2;

then A240: i in dom g1 by A237, FINSEQ_3:25;

1 <= i + 1 by NAT_1:11;

then i + 1 in dom g1 by A239, FINSEQ_3:25;

then X = LSeg (g1,i) by A236, A240, TOPREAL3:18;

then X in { (LSeg (g1,j)) where j is Nat : ( 1 <= j & j + 1 <= len g1 ) } by A237, A239;

then A241: x in L~ (f | k) by A36, A234, TARSKI:def 4;

L~ (f | k) c= L~ f by TOPREAL3:20;

hence x in L~ f by A241; :: thesis: verum

end;then i <= len g1 by A239, XXREAL_0:2;

then A240: i in dom g1 by A237, FINSEQ_3:25;

1 <= i + 1 by NAT_1:11;

then i + 1 in dom g1 by A239, FINSEQ_3:25;

then X = LSeg (g1,i) by A236, A240, TOPREAL3:18;

then X in { (LSeg (g1,j)) where j is Nat : ( 1 <= j & j + 1 <= len g1 ) } by A237, A239;

then A241: x in L~ (f | k) by A36, A234, TARSKI:def 4;

L~ (f | k) c= L~ f by TOPREAL3:20;

hence x in L~ f by A241; :: thesis: verum

suppose A242:
i + 1 > len g1
; :: thesis: x in L~ f

reconsider q1 = g /. i, q2 = g /. (i + 1) as Point of (TOP-REAL 2) ;

A243: i <= len g by A238, NAT_1:13;

A244: len g1 <= i by A242, NAT_1:13;

then A245: q1 `1 = (G * (i1,i2)) `1 by A212, A243;

A246: q1 `2 <= (G * (i1,j2)) `2 by A212, A244, A243;

A247: (G * (i1,i2)) `2 <= q1 `2 by A212, A244, A243;

q2 `1 = (G * (i1,i2)) `1 by A212, A238, A242;

then A248: q2 = |[(q1 `1),(q2 `2)]| by A245, EUCLID:53;

A249: q2 `2 <= (G * (i1,j2)) `2 by A212, A238, A242;

A250: ( q1 = |[(q1 `1),(q1 `2)]| & LSeg (g,i) = LSeg (q2,q1) ) by A237, A238, EUCLID:53, TOPREAL1:def 3;

A251: (G * (i1,i2)) `2 <= q2 `2 by A212, A238, A242;

end;A243: i <= len g by A238, NAT_1:13;

A244: len g1 <= i by A242, NAT_1:13;

then A245: q1 `1 = (G * (i1,i2)) `1 by A212, A243;

A246: q1 `2 <= (G * (i1,j2)) `2 by A212, A244, A243;

A247: (G * (i1,i2)) `2 <= q1 `2 by A212, A244, A243;

q2 `1 = (G * (i1,i2)) `1 by A212, A238, A242;

then A248: q2 = |[(q1 `1),(q2 `2)]| by A245, EUCLID:53;

A249: q2 `2 <= (G * (i1,j2)) `2 by A212, A238, A242;

A250: ( q1 = |[(q1 `1),(q1 `2)]| & LSeg (g,i) = LSeg (q2,q1) ) by A237, A238, EUCLID:53, TOPREAL1:def 3;

A251: (G * (i1,i2)) `2 <= q2 `2 by A212, A238, A242;

now :: thesis: x in L~ fend;

hence
x in L~ f
; :: thesis: verumper cases
( q1 `2 > q2 `2 or q1 `2 = q2 `2 or q1 `2 < q2 `2 )
by XXREAL_0:1;

end;

suppose
q1 `2 > q2 `2
; :: thesis: x in L~ f

then
LSeg (g,i) = { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `1 = q1 `1 & q2 `2 <= p2 `2 & p2 `2 <= q1 `2 ) }
by A248, A250, TOPREAL3:9;

then consider p2 being Point of (TOP-REAL 2) such that

A252: ( p2 = x & p2 `1 = q1 `1 ) and

A253: ( q2 `2 <= p2 `2 & p2 `2 <= q1 `2 ) by A234, A236;

( (G * (i1,i2)) `2 <= p2 `2 & p2 `2 <= (G * (i1,j2)) `2 ) by A246, A251, A253, XXREAL_0:2;

then A254: x in LSeg (f,k) by A209, A245, A252;

LSeg (f,k) in { (LSeg (f,j)) where j is Nat : ( 1 <= j & j + 1 <= len f ) } by A3, A13;

hence x in L~ f by A254, TARSKI:def 4; :: thesis: verum

end;then consider p2 being Point of (TOP-REAL 2) such that

A252: ( p2 = x & p2 `1 = q1 `1 ) and

A253: ( q2 `2 <= p2 `2 & p2 `2 <= q1 `2 ) by A234, A236;

( (G * (i1,i2)) `2 <= p2 `2 & p2 `2 <= (G * (i1,j2)) `2 ) by A246, A251, A253, XXREAL_0:2;

then A254: x in LSeg (f,k) by A209, A245, A252;

LSeg (f,k) in { (LSeg (f,j)) where j is Nat : ( 1 <= j & j + 1 <= len f ) } by A3, A13;

hence x in L~ f by A254, TARSKI:def 4; :: thesis: verum

suppose
q1 `2 = q2 `2
; :: thesis: x in L~ f

then
LSeg (g,i) = {q1}
by A248, A250, RLTOPSP1:70;

then x = q1 by A234, A236, TARSKI:def 1;

then A255: x in LSeg (f,k) by A209, A245, A247, A246;

LSeg (f,k) in { (LSeg (f,j)) where j is Nat : ( 1 <= j & j + 1 <= len f ) } by A3, A13;

hence x in L~ f by A255, TARSKI:def 4; :: thesis: verum

end;then x = q1 by A234, A236, TARSKI:def 1;

then A255: x in LSeg (f,k) by A209, A245, A247, A246;

LSeg (f,k) in { (LSeg (f,j)) where j is Nat : ( 1 <= j & j + 1 <= len f ) } by A3, A13;

hence x in L~ f by A255, TARSKI:def 4; :: thesis: verum

suppose
q1 `2 < q2 `2
; :: thesis: x in L~ f

then
LSeg (g,i) = { p1 where p1 is Point of (TOP-REAL 2) : ( p1 `1 = q1 `1 & q1 `2 <= p1 `2 & p1 `2 <= q2 `2 ) }
by A248, A250, TOPREAL3:9;

then consider p2 being Point of (TOP-REAL 2) such that

A256: ( p2 = x & p2 `1 = q1 `1 ) and

A257: ( q1 `2 <= p2 `2 & p2 `2 <= q2 `2 ) by A234, A236;

( (G * (i1,i2)) `2 <= p2 `2 & p2 `2 <= (G * (i1,j2)) `2 ) by A247, A249, A257, XXREAL_0:2;

then A258: x in LSeg (f,k) by A209, A245, A256;

LSeg (f,k) in { (LSeg (f,j)) where j is Nat : ( 1 <= j & j + 1 <= len f ) } by A3, A13;

hence x in L~ f by A258, TARSKI:def 4; :: thesis: verum

end;then consider p2 being Point of (TOP-REAL 2) such that

A256: ( p2 = x & p2 `1 = q1 `1 ) and

A257: ( q1 `2 <= p2 `2 & p2 `2 <= q2 `2 ) by A234, A236;

( (G * (i1,i2)) `2 <= p2 `2 & p2 `2 <= (G * (i1,j2)) `2 ) by A247, A249, A257, XXREAL_0:2;

then A258: x in LSeg (f,k) by A209, A245, A256;

LSeg (f,k) in { (LSeg (f,j)) where j is Nat : ( 1 <= j & j + 1 <= len f ) } by A3, A13;

hence x in L~ f by A258, TARSKI:def 4; :: thesis: verum

assume x in L~ f ; :: thesis: x in L~ g

then A259: x in (L~ (f | k)) \/ (LSeg (f,k)) by A3, A12, Th3;

now :: thesis: x in L~ gend;

hence
x in L~ g
; :: thesis: verumper cases
( x in L~ (f | k) or x in LSeg (f,k) )
by A259, XBOOLE_0:def 3;

end;

suppose
x in LSeg (f,k)
; :: thesis: x in L~ g

then consider p1 being Point of (TOP-REAL 2) such that

A261: p1 = x and

A262: p1 `1 = (G * (i1,i2)) `1 and

A263: (G * (i1,i2)) `2 <= p1 `2 and

A264: p1 `2 <= (G * (i1,j2)) `2 by A209;

defpred S_{2}[ Nat] means ( len g1 <= $1 & $1 <= len g & ( for q being Point of (TOP-REAL 2) st q = g /. $1 holds

q `2 <= p1 `2 ) );

_{2}[n] holds

n <= len g ;

consider ma being Nat such that

A268: ( S_{2}[ma] & ( for n being Nat st S_{2}[n] holds

n <= ma ) ) from NAT_1:sch 6(A267, A265);

reconsider ma = ma as Element of NAT by ORDINAL1:def 12;

end;A261: p1 = x and

A262: p1 `1 = (G * (i1,i2)) `1 and

A263: (G * (i1,i2)) `2 <= p1 `2 and

A264: p1 `2 <= (G * (i1,j2)) `2 by A209;

defpred S

q `2 <= p1 `2 ) );

A265: now :: thesis: ex n being Nat st S_{2}[n]

A267:
for n being Nat st Sreconsider n = len g1 as Nat ;

take n = n; :: thesis: S_{2}[n]

thus S_{2}[n]
:: thesis: verum

end;take n = n; :: thesis: S

thus S

proof

thus
( len g1 <= n & n <= len g )
by A211, XREAL_1:31; :: thesis: for q being Point of (TOP-REAL 2) st q = g /. n holds

q `2 <= p1 `2

1 <= len g1 by A13, A23, A39, XXREAL_0:2;

then A266: len g1 in dom g1 by FINSEQ_3:25;

let q be Point of (TOP-REAL 2); :: thesis: ( q = g /. n implies q `2 <= p1 `2 )

assume q = g /. n ; :: thesis: q `2 <= p1 `2

then q = (f | k) /. (len (f | k)) by A38, A266, FINSEQ_4:68

.= G * (i1,i2) by A17, A23, A14, A19, FINSEQ_4:71 ;

hence q `2 <= p1 `2 by A263; :: thesis: verum

end;q `2 <= p1 `2

1 <= len g1 by A13, A23, A39, XXREAL_0:2;

then A266: len g1 in dom g1 by FINSEQ_3:25;

let q be Point of (TOP-REAL 2); :: thesis: ( q = g /. n implies q `2 <= p1 `2 )

assume q = g /. n ; :: thesis: q `2 <= p1 `2

then q = (f | k) /. (len (f | k)) by A38, A266, FINSEQ_4:68

.= G * (i1,i2) by A17, A23, A14, A19, FINSEQ_4:71 ;

hence q `2 <= p1 `2 by A263; :: thesis: verum

n <= len g ;

consider ma being Nat such that

A268: ( S

n <= ma ) ) from NAT_1:sch 6(A267, A265);

reconsider ma = ma as Element of NAT by ORDINAL1:def 12;

now :: thesis: x in L~ gend;

hence
x in L~ g
; :: thesis: verumper cases
( ma = len g or ma <> len g )
;

end;

suppose A269:
ma = len g
; :: thesis: x in L~ g

i2 + 1 <= j2
by A176, NAT_1:13;

then A270: 1 <= l by XREAL_1:19;

then 0 + 1 <= ma by A178, A211, A269, XREAL_1:7;

then reconsider m1 = ma - 1 as Element of NAT by INT_1:5;

A271: m1 + 1 = ma ;

(len g1) + 1 <= ma by A178, A211, A269, A270, XREAL_1:7;

then A272: m1 >= len g1 by A271, XREAL_1:6;

reconsider q = g /. m1 as Point of (TOP-REAL 2) ;

set lq = { e where e is Point of (TOP-REAL 2) : ( e `1 = (G * (i1,i2)) `1 & q `2 <= e `2 & e `2 <= (G * (i1,j2)) `2 ) } ;

A273: i2 + l = j2 ;

A274: l in dom g2 by A178, A270, FINSEQ_3:25;

then A275: g /. ma = g2 /. l by A178, A211, A269, FINSEQ_4:69

.= G * (i1,j2) by A178, A274, A273 ;

then (G * (i1,j2)) `2 <= p1 `2 by A268;

then A276: p1 `2 = (G * (i1,j2)) `2 by A264, XXREAL_0:1;

A277: m1 <= len g by A269, A271, NAT_1:11;

then A278: q `1 = (G * (i1,i2)) `1 by A212, A272;

A279: q `2 <= (G * (i1,j2)) `2 by A212, A272, A277;

1 <= len g1 by A13, A23, A39, XXREAL_0:2;

then A280: 1 <= m1 by A272, XXREAL_0:2;

then ( q = |[(q `1),(q `2)]| & LSeg (g,m1) = LSeg ((G * (i1,j2)),q) ) by A269, A275, A271, EUCLID:53, TOPREAL1:def 3;

then LSeg (g,m1) = { e where e is Point of (TOP-REAL 2) : ( e `1 = (G * (i1,i2)) `1 & q `2 <= e `2 & e `2 <= (G * (i1,j2)) `2 ) } by A208, A201, A278, A279, TOPREAL3:9;

then A281: p1 in LSeg (g,m1) by A262, A276, A279;

LSeg (g,m1) in { (LSeg (g,i)) where i is Nat : ( 1 <= i & i + 1 <= len g ) } by A269, A271, A280;

hence x in L~ g by A261, A281, TARSKI:def 4; :: thesis: verum

end;then A270: 1 <= l by XREAL_1:19;

then 0 + 1 <= ma by A178, A211, A269, XREAL_1:7;

then reconsider m1 = ma - 1 as Element of NAT by INT_1:5;

A271: m1 + 1 = ma ;

(len g1) + 1 <= ma by A178, A211, A269, A270, XREAL_1:7;

then A272: m1 >= len g1 by A271, XREAL_1:6;

reconsider q = g /. m1 as Point of (TOP-REAL 2) ;

set lq = { e where e is Point of (TOP-REAL 2) : ( e `1 = (G * (i1,i2)) `1 & q `2 <= e `2 & e `2 <= (G * (i1,j2)) `2 ) } ;

A273: i2 + l = j2 ;

A274: l in dom g2 by A178, A270, FINSEQ_3:25;

then A275: g /. ma = g2 /. l by A178, A211, A269, FINSEQ_4:69

.= G * (i1,j2) by A178, A274, A273 ;

then (G * (i1,j2)) `2 <= p1 `2 by A268;

then A276: p1 `2 = (G * (i1,j2)) `2 by A264, XXREAL_0:1;

A277: m1 <= len g by A269, A271, NAT_1:11;

then A278: q `1 = (G * (i1,i2)) `1 by A212, A272;

A279: q `2 <= (G * (i1,j2)) `2 by A212, A272, A277;

1 <= len g1 by A13, A23, A39, XXREAL_0:2;

then A280: 1 <= m1 by A272, XXREAL_0:2;

then ( q = |[(q `1),(q `2)]| & LSeg (g,m1) = LSeg ((G * (i1,j2)),q) ) by A269, A275, A271, EUCLID:53, TOPREAL1:def 3;

then LSeg (g,m1) = { e where e is Point of (TOP-REAL 2) : ( e `1 = (G * (i1,i2)) `1 & q `2 <= e `2 & e `2 <= (G * (i1,j2)) `2 ) } by A208, A201, A278, A279, TOPREAL3:9;

then A281: p1 in LSeg (g,m1) by A262, A276, A279;

LSeg (g,m1) in { (LSeg (g,i)) where i is Nat : ( 1 <= i & i + 1 <= len g ) } by A269, A271, A280;

hence x in L~ g by A261, A281, TARSKI:def 4; :: thesis: verum

suppose
ma <> len g
; :: thesis: x in L~ g

then
ma < len g
by A268, XXREAL_0:1;

then A282: ma + 1 <= len g by NAT_1:13;

reconsider qa = g /. ma, qa1 = g /. (ma + 1) as Point of (TOP-REAL 2) ;

set lma = { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `1 = (G * (i1,i2)) `1 & qa `2 <= p2 `2 & p2 `2 <= qa1 `2 ) } ;

A283: qa1 = |[(qa1 `1),(qa1 `2)]| by EUCLID:53;

A284: qa `2 <= p1 `2 by A268;

A285: len g1 <= ma + 1 by A268, NAT_1:13;

then A286: qa1 `1 = (G * (i1,i2)) `1 by A212, A282;

A289: 1 <= ma by A13, A23, A39, A268, NAT_1:13;

then LSeg (g,ma) = LSeg (qa,qa1) by A282, TOPREAL1:def 3

.= { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `1 = (G * (i1,i2)) `1 & qa `2 <= p2 `2 & p2 `2 <= qa1 `2 ) } by A284, A287, A286, A288, A283, TOPREAL3:9, XXREAL_0:2 ;

then A290: x in LSeg (g,ma) by A261, A262, A284, A287;

LSeg (g,ma) in { (LSeg (g,i)) where i is Nat : ( 1 <= i & i + 1 <= len g ) } by A289, A282;

hence x in L~ g by A290, TARSKI:def 4; :: thesis: verum

end;then A282: ma + 1 <= len g by NAT_1:13;

reconsider qa = g /. ma, qa1 = g /. (ma + 1) as Point of (TOP-REAL 2) ;

set lma = { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `1 = (G * (i1,i2)) `1 & qa `2 <= p2 `2 & p2 `2 <= qa1 `2 ) } ;

A283: qa1 = |[(qa1 `1),(qa1 `2)]| by EUCLID:53;

A284: qa `2 <= p1 `2 by A268;

A285: len g1 <= ma + 1 by A268, NAT_1:13;

then A286: qa1 `1 = (G * (i1,i2)) `1 by A212, A282;

A287: now :: thesis: not qa1 `2 <= p1 `2

A288:
( qa `1 = (G * (i1,i2)) `1 & qa = |[(qa `1),(qa `2)]| )
by A212, A268, EUCLID:53;assume
qa1 `2 <= p1 `2
; :: thesis: contradiction

then for q being Point of (TOP-REAL 2) st q = g /. (ma + 1) holds

q `2 <= p1 `2 ;

then ma + 1 <= ma by A268, A282, A285;

hence contradiction by XREAL_1:29; :: thesis: verum

end;then for q being Point of (TOP-REAL 2) st q = g /. (ma + 1) holds

q `2 <= p1 `2 ;

then ma + 1 <= ma by A268, A282, A285;

hence contradiction by XREAL_1:29; :: thesis: verum

A289: 1 <= ma by A13, A23, A39, A268, NAT_1:13;

then LSeg (g,ma) = LSeg (qa,qa1) by A282, TOPREAL1:def 3

.= { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `1 = (G * (i1,i2)) `1 & qa `2 <= p2 `2 & p2 `2 <= qa1 `2 ) } by A284, A287, A286, A288, A283, TOPREAL3:9, XXREAL_0:2 ;

then A290: x in LSeg (g,ma) by A261, A262, A284, A287;

LSeg (g,ma) in { (LSeg (g,i)) where i is Nat : ( 1 <= i & i + 1 <= len g ) } by A289, A282;

hence x in L~ g by A290, TARSKI:def 4; :: thesis: verum

then 1 in dom g1 by FINSEQ_3:25;

hence g /. 1 = (f | k) /. 1 by A37, FINSEQ_4:68

.= f /. 1 by A17, A15, FINSEQ_4:71 ;

:: thesis: ( g /. (len g) = f /. (len f) & len f <= len g )

A291: len g = (len g1) + l by A178, FINSEQ_1:22;

i2 + 1 <= j2 by A176, NAT_1:13;

then A292: 1 <= l by XREAL_1:19;

then A293: l in dom g2 by A178, A184, FINSEQ_1:1;

hence g /. (len g) = g2 /. l by A291, FINSEQ_4:69

.= G * (i1,(i2 + l)) by A178, A293

.= f /. (len f) by A3, A46, A58 ;

:: thesis: len f <= len g

thus len f <= len g by A3, A23, A39, A292, A291, XREAL_1:7; :: thesis: verum

( g is_sequence_on G & L~ f = L~ g & g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g ) ; :: thesis: verum

suppose A294:
i2 = j2
; :: thesis: ex g being FinSequence of (TOP-REAL 2) st

( g is_sequence_on G & L~ f = L~ g & g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g )

( g is_sequence_on G & L~ f = L~ g & g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g )

set ppi = G * (i1,i2);

set pj = G * (j1,i2);

set pj = G * (j1,i2);

now :: thesis: ( ( i1 > j1 & ex g being FinSequence of the carrier of (TOP-REAL 2) st

( g is_sequence_on G & L~ g = L~ f & g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g ) ) or ( i1 = j1 & contradiction ) or ( i1 < j1 & ex g being FinSequence of the carrier of (TOP-REAL 2) st

( g is_sequence_on G & L~ g = L~ f & g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g ) ) )

( g is_sequence_on G & L~ g = L~ f & g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g ) ) or ( i1 = j1 & contradiction ) or ( i1 < j1 & ex g being FinSequence of the carrier of (TOP-REAL 2) st

( g is_sequence_on G & L~ g = L~ f & g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g ) ) )

per cases
( i1 > j1 or i1 = j1 or i1 < j1 )
by XXREAL_0:1;

case A295:
i1 > j1
; :: thesis: ex g being FinSequence of the carrier of (TOP-REAL 2) st

( g is_sequence_on G & L~ g = L~ f & g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g )

( g is_sequence_on G & L~ g = L~ f & g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g )

c1 /. j1 = c1 . j1
by A48, A43, PARTFUN1:def 6;

then A296: c1 /. j1 = G * (j1,i2) by A48, MATRIX_0:def 8;

then A297: (X_axis c1) . j1 = (G * (j1,i2)) `1 by A48, A43, A22, GOBOARD1:def 1;

c1 /. i1 = c1 . i1 by A49, A43, PARTFUN1:def 6;

then A298: c1 /. i1 = G * (i1,i2) by A49, MATRIX_0:def 8;

then A299: (X_axis c1) . i1 = (G * (i1,i2)) `1 by A49, A43, A22, GOBOARD1:def 1;

then A300: (G * (j1,i2)) `1 < (G * (i1,i2)) `1 by A49, A48, A52, A43, A22, A295, A297, SEQM_3:def 1;

A301: (Y_axis c1) . j1 = (G * (j1,i2)) `2 by A48, A43, A21, A296, GOBOARD1:def 2;

(Y_axis c1) . i1 = (G * (i1,i2)) `2 by A49, A43, A21, A298, GOBOARD1:def 2;

then A302: (G * (i1,i2)) `2 = (G * (j1,i2)) `2 by A49, A48, A53, A43, A21, A301, SEQM_3:def 10;

reconsider l = i1 - j1 as Element of NAT by A295, INT_1:5;

defpred S_{2}[ Nat, set ] means for m being Nat st m = i1 - $1 holds

$2 = G * (m,i2);

set lk = { w where w is Point of (TOP-REAL 2) : ( w `2 = (G * (i1,i2)) `2 & (G * (j1,i2)) `1 <= w `1 & w `1 <= (G * (i1,i2)) `1 ) } ;

A303: G * (i1,i2) = |[((G * (i1,i2)) `1),((G * (i1,i2)) `2)]| by EUCLID:53;

A309: ( len g2 = l & ( for n being Nat st n in Seg l holds

S_{2}[n,g2 /. n] ) )
from FINSEQ_4:sch 1(A308);

take g = g1 ^ g2; :: thesis: ( g is_sequence_on G & L~ g = L~ f & g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g )

A310: dom g2 = Seg l by A309, FINSEQ_1:def 3;

ex i, j being Nat st

( [i,j] in Indices G & g /. n = G * (i,j) ) by A40, GOBOARD1:23;

for m, k, i, j being Nat st [m,k] in Indices G & [i,j] in Indices G & g /. n = G * (m,k) & g /. (n + 1) = G * (i,j) holds

|.(m - i).| + |.(k - j).| = 1 by A41, A311, GOBOARD1:24;

hence g is_sequence_on G by A320; :: thesis: ( L~ g = L~ f & g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g )

reconsider m1 = i1 - l as Element of NAT by ORDINAL1:def 12;

A327: G * (j1,i2) = |[((G * (j1,i2)) `1),((G * (j1,i2)) `2)]| by EUCLID:53;

A328: LSeg (f,k) = LSeg ((G * (j1,i2)),(G * (i1,i2))) by A3, A13, A19, A46, A294, TOPREAL1:def 3

.= { w where w is Point of (TOP-REAL 2) : ( w `2 = (G * (i1,i2)) `2 & (G * (j1,i2)) `1 <= w `1 & w `1 <= (G * (i1,i2)) `1 ) } by A300, A302, A303, A327, TOPREAL3:10 ;

thus L~ g = L~ f :: thesis: ( g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g )

then A296: c1 /. j1 = G * (j1,i2) by A48, MATRIX_0:def 8;

then A297: (X_axis c1) . j1 = (G * (j1,i2)) `1 by A48, A43, A22, GOBOARD1:def 1;

c1 /. i1 = c1 . i1 by A49, A43, PARTFUN1:def 6;

then A298: c1 /. i1 = G * (i1,i2) by A49, MATRIX_0:def 8;

then A299: (X_axis c1) . i1 = (G * (i1,i2)) `1 by A49, A43, A22, GOBOARD1:def 1;

then A300: (G * (j1,i2)) `1 < (G * (i1,i2)) `1 by A49, A48, A52, A43, A22, A295, A297, SEQM_3:def 1;

A301: (Y_axis c1) . j1 = (G * (j1,i2)) `2 by A48, A43, A21, A296, GOBOARD1:def 2;

(Y_axis c1) . i1 = (G * (i1,i2)) `2 by A49, A43, A21, A298, GOBOARD1:def 2;

then A302: (G * (i1,i2)) `2 = (G * (j1,i2)) `2 by A49, A48, A53, A43, A21, A301, SEQM_3:def 10;

reconsider l = i1 - j1 as Element of NAT by A295, INT_1:5;

defpred S

$2 = G * (m,i2);

set lk = { w where w is Point of (TOP-REAL 2) : ( w `2 = (G * (i1,i2)) `2 & (G * (j1,i2)) `1 <= w `1 & w `1 <= (G * (i1,i2)) `1 ) } ;

A303: G * (i1,i2) = |[((G * (i1,i2)) `1),((G * (i1,i2)) `2)]| by EUCLID:53;

A304: now :: thesis: for n being Nat st n in Seg l holds

( i1 - n is Element of NAT & [(i1 - n),i2] in Indices G & i1 - n in dom G )

( i1 - n is Element of NAT & [(i1 - n),i2] in Indices G & i1 - n in dom G )

let n be Nat; :: thesis: ( n in Seg l implies ( i1 - n is Element of NAT & [(i1 - n),i2] in Indices G & i1 - n in dom G ) )

assume n in Seg l ; :: thesis: ( i1 - n is Element of NAT & [(i1 - n),i2] in Indices G & i1 - n in dom G )

then A305: n <= l by FINSEQ_1:1;

l <= i1 by XREAL_1:43;

then reconsider w = i1 - n as Element of NAT by A305, INT_1:5, XXREAL_0:2;

( i1 - n <= i1 & i1 <= len G ) by A49, FINSEQ_3:25, XREAL_1:43;

then A306: w <= len G by XXREAL_0:2;

A307: 1 <= j1 by A48, FINSEQ_3:25;

i1 - l <= i1 - n by A305, XREAL_1:13;

then 1 <= w by A307, XXREAL_0:2;

then w in dom G by A306, FINSEQ_3:25;

hence ( i1 - n is Element of NAT & [(i1 - n),i2] in Indices G & i1 - n in dom G ) by A47, A51, ZFMISC_1:87; :: thesis: verum

end;assume n in Seg l ; :: thesis: ( i1 - n is Element of NAT & [(i1 - n),i2] in Indices G & i1 - n in dom G )

then A305: n <= l by FINSEQ_1:1;

l <= i1 by XREAL_1:43;

then reconsider w = i1 - n as Element of NAT by A305, INT_1:5, XXREAL_0:2;

( i1 - n <= i1 & i1 <= len G ) by A49, FINSEQ_3:25, XREAL_1:43;

then A306: w <= len G by XXREAL_0:2;

A307: 1 <= j1 by A48, FINSEQ_3:25;

i1 - l <= i1 - n by A305, XREAL_1:13;

then 1 <= w by A307, XXREAL_0:2;

then w in dom G by A306, FINSEQ_3:25;

hence ( i1 - n is Element of NAT & [(i1 - n),i2] in Indices G & i1 - n in dom G ) by A47, A51, ZFMISC_1:87; :: thesis: verum

A308: now :: thesis: for n being Nat st n in Seg l holds

ex p being Element of the carrier of (TOP-REAL 2) st S_{2}[n,p]

consider g2 being FinSequence of (TOP-REAL 2) such that ex p being Element of the carrier of (TOP-REAL 2) st S

let n be Nat; :: thesis: ( n in Seg l implies ex p being Element of the carrier of (TOP-REAL 2) st S_{2}[n,p] )

assume n in Seg l ; :: thesis: ex p being Element of the carrier of (TOP-REAL 2) st S_{2}[n,p]

then reconsider m = i1 - n as Element of NAT by A304;

take p = G * (m,i2); :: thesis: S_{2}[n,p]

thus S_{2}[n,p]
; :: thesis: verum

end;assume n in Seg l ; :: thesis: ex p being Element of the carrier of (TOP-REAL 2) st S

then reconsider m = i1 - n as Element of NAT by A304;

take p = G * (m,i2); :: thesis: S

thus S

A309: ( len g2 = l & ( for n being Nat st n in Seg l holds

S

take g = g1 ^ g2; :: thesis: ( g is_sequence_on G & L~ g = L~ f & g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g )

A310: dom g2 = Seg l by A309, FINSEQ_1:def 3;

A311: now :: thesis: for n being Nat st n in dom g2 & n + 1 in dom g2 holds

for l1, l2, l3, l4 being Nat st [l1,l2] in Indices G & [l3,l4] in Indices G & g2 /. n = G * (l1,l2) & g2 /. (n + 1) = G * (l3,l4) holds

|.(l1 - l3).| + |.(l2 - l4).| = 1

for l1, l2, l3, l4 being Nat st [l1,l2] in Indices G & [l3,l4] in Indices G & g2 /. n = G * (l1,l2) & g2 /. (n + 1) = G * (l3,l4) holds

|.(l1 - l3).| + |.(l2 - l4).| = 1

let n be Nat; :: thesis: ( n in dom g2 & n + 1 in dom g2 implies for l1, l2, l3, l4 being Nat st [l1,l2] in Indices G & [l3,l4] in Indices G & g2 /. n = G * (l1,l2) & g2 /. (n + 1) = G * (l3,l4) holds

|.(l1 - l3).| + |.(l2 - l4).| = 1 )

assume that

A312: n in dom g2 and

A313: n + 1 in dom g2 ; :: thesis: for l1, l2, l3, l4 being Nat st [l1,l2] in Indices G & [l3,l4] in Indices G & g2 /. n = G * (l1,l2) & g2 /. (n + 1) = G * (l3,l4) holds

|.(l1 - l3).| + |.(l2 - l4).| = 1

reconsider m1 = i1 - n, m2 = i1 - (n + 1) as Element of NAT by A304, A310, A312, A313;

let l1, l2, l3, l4 be Nat; :: thesis: ( [l1,l2] in Indices G & [l3,l4] in Indices G & g2 /. n = G * (l1,l2) & g2 /. (n + 1) = G * (l3,l4) implies |.(l1 - l3).| + |.(l2 - l4).| = 1 )

assume that

A314: [l1,l2] in Indices G and

A315: [l3,l4] in Indices G and

A316: g2 /. n = G * (l1,l2) and

A317: g2 /. (n + 1) = G * (l3,l4) ; :: thesis: |.(l1 - l3).| + |.(l2 - l4).| = 1

( [(i1 - (n + 1)),i2] in Indices G & g2 /. (n + 1) = G * (m2,i2) ) by A304, A309, A310, A313;

then A318: ( l3 = m2 & l4 = i2 ) by A315, A317, GOBOARD1:5;

( [(i1 - n),i2] in Indices G & g2 /. n = G * (m1,i2) ) by A304, A309, A310, A312;

then ( l1 = m1 & l2 = i2 ) by A314, A316, GOBOARD1:5;

hence |.(l1 - l3).| + |.(l2 - l4).| = |.((i1 - n) - (i1 - (n + 1))).| + 0 by A318, ABSVALUE:2

.= 1 by ABSVALUE:def 1 ;

:: thesis: verum

end;|.(l1 - l3).| + |.(l2 - l4).| = 1 )

assume that

A312: n in dom g2 and

A313: n + 1 in dom g2 ; :: thesis: for l1, l2, l3, l4 being Nat st [l1,l2] in Indices G & [l3,l4] in Indices G & g2 /. n = G * (l1,l2) & g2 /. (n + 1) = G * (l3,l4) holds

|.(l1 - l3).| + |.(l2 - l4).| = 1

reconsider m1 = i1 - n, m2 = i1 - (n + 1) as Element of NAT by A304, A310, A312, A313;

let l1, l2, l3, l4 be Nat; :: thesis: ( [l1,l2] in Indices G & [l3,l4] in Indices G & g2 /. n = G * (l1,l2) & g2 /. (n + 1) = G * (l3,l4) implies |.(l1 - l3).| + |.(l2 - l4).| = 1 )

assume that

A314: [l1,l2] in Indices G and

A315: [l3,l4] in Indices G and

A316: g2 /. n = G * (l1,l2) and

A317: g2 /. (n + 1) = G * (l3,l4) ; :: thesis: |.(l1 - l3).| + |.(l2 - l4).| = 1

( [(i1 - (n + 1)),i2] in Indices G & g2 /. (n + 1) = G * (m2,i2) ) by A304, A309, A310, A313;

then A318: ( l3 = m2 & l4 = i2 ) by A315, A317, GOBOARD1:5;

( [(i1 - n),i2] in Indices G & g2 /. n = G * (m1,i2) ) by A304, A309, A310, A312;

then ( l1 = m1 & l2 = i2 ) by A314, A316, GOBOARD1:5;

hence |.(l1 - l3).| + |.(l2 - l4).| = |.((i1 - n) - (i1 - (n + 1))).| + 0 by A318, ABSVALUE:2

.= 1 by ABSVALUE:def 1 ;

:: thesis: verum

now :: thesis: for n being Nat st n in dom g2 holds

ex m, k being Nat st

( [m,k] in Indices G & g2 /. n = G * (m,k) )

then A320:
for n being Nat st n in dom g holds ex m, k being Nat st

( [m,k] in Indices G & g2 /. n = G * (m,k) )

let n be Nat; :: thesis: ( n in dom g2 implies ex m, k being Nat st

( [m,k] in Indices G & g2 /. n = G * (m,k) ) )

assume A319: n in dom g2 ; :: thesis: ex m, k being Nat st

( [m,k] in Indices G & g2 /. n = G * (m,k) )

then reconsider m = i1 - n as Element of NAT by A304, A310;

reconsider m = m, k = i2 as Nat ;

take m = m; :: thesis: ex k being Nat st

( [m,k] in Indices G & g2 /. n = G * (m,k) )

take k = k; :: thesis: ( [m,k] in Indices G & g2 /. n = G * (m,k) )

thus ( [m,k] in Indices G & g2 /. n = G * (m,k) ) by A304, A309, A310, A319; :: thesis: verum

end;( [m,k] in Indices G & g2 /. n = G * (m,k) ) )

assume A319: n in dom g2 ; :: thesis: ex m, k being Nat st

( [m,k] in Indices G & g2 /. n = G * (m,k) )

then reconsider m = i1 - n as Element of NAT by A304, A310;

reconsider m = m, k = i2 as Nat ;

take m = m; :: thesis: ex k being Nat st

( [m,k] in Indices G & g2 /. n = G * (m,k) )

take k = k; :: thesis: ( [m,k] in Indices G & g2 /. n = G * (m,k) )

thus ( [m,k] in Indices G & g2 /. n = G * (m,k) ) by A304, A309, A310, A319; :: thesis: verum

ex i, j being Nat st

( [i,j] in Indices G & g /. n = G * (i,j) ) by A40, GOBOARD1:23;

now :: thesis: for l1, l2, l3, l4 being Nat st [l1,l2] in Indices G & [l3,l4] in Indices G & g1 /. (len g1) = G * (l1,l2) & g2 /. 1 = G * (l3,l4) & len g1 in dom g1 & 1 in dom g2 holds

|.(l1 - l3).| + |.(l2 - l4).| = 1

then
for n being Nat st n in dom g & n + 1 in dom g holds |.(l1 - l3).| + |.(l2 - l4).| = 1

let l1, l2, l3, l4 be Nat; :: thesis: ( [l1,l2] in Indices G & [l3,l4] in Indices G & g1 /. (len g1) = G * (l1,l2) & g2 /. 1 = G * (l3,l4) & len g1 in dom g1 & 1 in dom g2 implies |.(l1 - l3).| + |.(l2 - l4).| = 1 )

assume that

A321: [l1,l2] in Indices G and

A322: [l3,l4] in Indices G and

A323: g1 /. (len g1) = G * (l1,l2) and

A324: g2 /. 1 = G * (l3,l4) and

len g1 in dom g1 and

A325: 1 in dom g2 ; :: thesis: |.(l1 - l3).| + |.(l2 - l4).| = 1

reconsider m1 = i1 - 1 as Element of NAT by A304, A310, A325;

( [(i1 - 1),i2] in Indices G & g2 /. 1 = G * (m1,i2) ) by A304, A309, A310, A325;

then A326: ( l3 = m1 & l4 = i2 ) by A322, A324, GOBOARD1:5;

(f | k) /. (len (f | k)) = f /. k by A17, A23, A14, FINSEQ_4:71;

then ( l1 = i1 & l2 = i2 ) by A38, A18, A19, A321, A323, GOBOARD1:5;

hence |.(l1 - l3).| + |.(l2 - l4).| = |.(i1 - (i1 - 1)).| + 0 by A326, ABSVALUE:2

.= 1 by ABSVALUE:def 1 ;

:: thesis: verum

end;assume that

A321: [l1,l2] in Indices G and

A322: [l3,l4] in Indices G and

A323: g1 /. (len g1) = G * (l1,l2) and

A324: g2 /. 1 = G * (l3,l4) and

len g1 in dom g1 and

A325: 1 in dom g2 ; :: thesis: |.(l1 - l3).| + |.(l2 - l4).| = 1

reconsider m1 = i1 - 1 as Element of NAT by A304, A310, A325;

( [(i1 - 1),i2] in Indices G & g2 /. 1 = G * (m1,i2) ) by A304, A309, A310, A325;

then A326: ( l3 = m1 & l4 = i2 ) by A322, A324, GOBOARD1:5;

(f | k) /. (len (f | k)) = f /. k by A17, A23, A14, FINSEQ_4:71;

then ( l1 = i1 & l2 = i2 ) by A38, A18, A19, A321, A323, GOBOARD1:5;

hence |.(l1 - l3).| + |.(l2 - l4).| = |.(i1 - (i1 - 1)).| + 0 by A326, ABSVALUE:2

.= 1 by ABSVALUE:def 1 ;

:: thesis: verum

for m, k, i, j being Nat st [m,k] in Indices G & [i,j] in Indices G & g /. n = G * (m,k) & g /. (n + 1) = G * (i,j) holds

|.(m - i).| + |.(k - j).| = 1 by A41, A311, GOBOARD1:24;

hence g is_sequence_on G by A320; :: thesis: ( L~ g = L~ f & g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g )

reconsider m1 = i1 - l as Element of NAT by ORDINAL1:def 12;

A327: G * (j1,i2) = |[((G * (j1,i2)) `1),((G * (j1,i2)) `2)]| by EUCLID:53;

A328: LSeg (f,k) = LSeg ((G * (j1,i2)),(G * (i1,i2))) by A3, A13, A19, A46, A294, TOPREAL1:def 3

.= { w where w is Point of (TOP-REAL 2) : ( w `2 = (G * (i1,i2)) `2 & (G * (j1,i2)) `1 <= w `1 & w `1 <= (G * (i1,i2)) `1 ) } by A300, A302, A303, A327, TOPREAL3:10 ;

thus L~ g = L~ f :: thesis: ( g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g )

proof

set lg = { (LSeg (g,i)) where i is Nat : ( 1 <= i & i + 1 <= len g ) } ;

set lf = { (LSeg (f,j)) where j is Nat : ( 1 <= j & j + 1 <= len f ) } ;

A329: len g = (len g1) + (len g2) by FINSEQ_1:22;

assume x in L~ f ; :: thesis: x in L~ g

then A376: x in (L~ (f | k)) \/ (LSeg (f,k)) by A3, A12, Th3;

set lf = { (LSeg (f,j)) where j is Nat : ( 1 <= j & j + 1 <= len f ) } ;

A329: len g = (len g1) + (len g2) by FINSEQ_1:22;

A330: now :: thesis: for j being Nat st len g1 <= j & j <= len g holds

for p being Point of (TOP-REAL 2) st p = g /. j holds

( p `2 = (G * (i1,i2)) `2 & (G * (j1,i2)) `1 <= p `1 & p `1 <= (G * (i1,i2)) `1 & p in rng c1 )

thus
L~ g c= L~ f
:: according to XBOOLE_0:def 10 :: thesis: L~ f c= L~ gfor p being Point of (TOP-REAL 2) st p = g /. j holds

( p `2 = (G * (i1,i2)) `2 & (G * (j1,i2)) `1 <= p `1 & p `1 <= (G * (i1,i2)) `1 & p in rng c1 )

let j be Nat; :: thesis: ( len g1 <= j & j <= len g implies for p being Point of (TOP-REAL 2) st p = g /. j holds

( p `2 = (G * (i1,i2)) `2 & (G * (j1,i2)) `1 <= p `1 & p `1 <= (G * (i1,i2)) `1 & p in rng c1 ) )

assume that

A331: len g1 <= j and

A332: j <= len g ; :: thesis: for p being Point of (TOP-REAL 2) st p = g /. j holds

( p `2 = (G * (i1,i2)) `2 & (G * (j1,i2)) `1 <= p `1 & p `1 <= (G * (i1,i2)) `1 & p in rng c1 )

reconsider w = j - (len g1) as Element of NAT by A331, INT_1:5;

let p be Point of (TOP-REAL 2); :: thesis: ( p = g /. j implies ( p `2 = (G * (i1,i2)) `2 & (G * (j1,i2)) `1 <= p `1 & p `1 <= (G * (i1,i2)) `1 & p in rng c1 ) )

assume A333: p = g /. j ; :: thesis: ( p `2 = (G * (i1,i2)) `2 & (G * (j1,i2)) `1 <= p `1 & p `1 <= (G * (i1,i2)) `1 & p in rng c1 )

end;( p `2 = (G * (i1,i2)) `2 & (G * (j1,i2)) `1 <= p `1 & p `1 <= (G * (i1,i2)) `1 & p in rng c1 ) )

assume that

A331: len g1 <= j and

A332: j <= len g ; :: thesis: for p being Point of (TOP-REAL 2) st p = g /. j holds

( p `2 = (G * (i1,i2)) `2 & (G * (j1,i2)) `1 <= p `1 & p `1 <= (G * (i1,i2)) `1 & p in rng c1 )

reconsider w = j - (len g1) as Element of NAT by A331, INT_1:5;

let p be Point of (TOP-REAL 2); :: thesis: ( p = g /. j implies ( p `2 = (G * (i1,i2)) `2 & (G * (j1,i2)) `1 <= p `1 & p `1 <= (G * (i1,i2)) `1 & p in rng c1 ) )

assume A333: p = g /. j ; :: thesis: ( p `2 = (G * (i1,i2)) `2 & (G * (j1,i2)) `1 <= p `1 & p `1 <= (G * (i1,i2)) `1 & p in rng c1 )

now :: thesis: ( p `2 = (G * (i1,i2)) `2 & (G * (j1,i2)) `1 <= p `1 & p `1 <= (G * (i1,i2)) `1 & p in rng c1 )end;

hence
( p `2 = (G * (i1,i2)) `2 & (G * (j1,i2)) `1 <= p `1 & p `1 <= (G * (i1,i2)) `1 & p in rng c1 )
; :: thesis: verumper cases
( j = len g1 or j <> len g1 )
;

end;

suppose A334:
j = len g1
; :: thesis: ( p `2 = (G * (i1,i2)) `2 & (G * (j1,i2)) `1 <= p `1 & p `1 <= (G * (i1,i2)) `1 & p in rng c1 )

1 <= len g1
by A13, A23, A39, XXREAL_0:2;

then len g1 in dom g1 by FINSEQ_3:25;

then A335: g /. (len g1) = (f | k) /. (len (f | k)) by A38, FINSEQ_4:68

.= G * (i1,i2) by A17, A23, A14, A19, FINSEQ_4:71 ;

hence p `2 = (G * (i1,i2)) `2 by A333, A334; :: thesis: ( (G * (j1,i2)) `1 <= p `1 & p `1 <= (G * (i1,i2)) `1 & p in rng c1 )

thus ( (G * (j1,i2)) `1 <= p `1 & p `1 <= (G * (i1,i2)) `1 ) by A49, A48, A52, A43, A22, A295, A299, A297, A333, A334, A335, SEQM_3:def 1; :: thesis: p in rng c1

thus p in rng c1 by A49, A43, A298, A333, A334, A335, PARTFUN2:2; :: thesis: verum

end;then len g1 in dom g1 by FINSEQ_3:25;

then A335: g /. (len g1) = (f | k) /. (len (f | k)) by A38, FINSEQ_4:68

.= G * (i1,i2) by A17, A23, A14, A19, FINSEQ_4:71 ;

hence p `2 = (G * (i1,i2)) `2 by A333, A334; :: thesis: ( (G * (j1,i2)) `1 <= p `1 & p `1 <= (G * (i1,i2)) `1 & p in rng c1 )

thus ( (G * (j1,i2)) `1 <= p `1 & p `1 <= (G * (i1,i2)) `1 ) by A49, A48, A52, A43, A22, A295, A299, A297, A333, A334, A335, SEQM_3:def 1; :: thesis: p in rng c1

thus p in rng c1 by A49, A43, A298, A333, A334, A335, PARTFUN2:2; :: thesis: verum

suppose A336:
j <> len g1
; :: thesis: ( p `2 = (G * (i1,i2)) `2 & (G * (j1,i2)) `1 <= p `1 & p `1 <= (G * (i1,i2)) `1 & p in rng c1 )

A337:
w + (len g1) = j
;

then A338: w <= len g2 by A329, A332, XREAL_1:6;

A339: j - (len g1) <> 0 by A336;

then A340: w >= 1 by NAT_1:14;

then A341: w in dom g2 by A338, FINSEQ_3:25;

then reconsider u = i1 - w as Element of NAT by A304, A310;

A342: g /. j = g2 /. w by A340, A337, A338, SEQ_4:136;

A343: u < i1 by A339, XREAL_1:44;

A344: g2 /. w = G * (u,i2) by A309, A310, A341;

A345: (Y_axis c1) . i1 = (G * (i1,i2)) `2 by A49, A43, A21, A298, GOBOARD1:def 2;

A346: i1 - w in dom G by A304, A310, A341;

c1 /. u = c1 . u by A43, A304, A310, A341, PARTFUN1:def 6;

then A347: c1 /. u = G * (u,i2) by A346, MATRIX_0:def 8;

then A348: (X_axis c1) . u = (G * (u,i2)) `1 by A43, A22, A346, GOBOARD1:def 1;

(Y_axis c1) . u = (G * (u,i2)) `2 by A43, A21, A346, A347, GOBOARD1:def 2;

hence p `2 = (G * (i1,i2)) `2 by A49, A53, A43, A21, A333, A342, A346, A344, A345, SEQM_3:def 10; :: thesis: ( (G * (j1,i2)) `1 <= p `1 & p `1 <= (G * (i1,i2)) `1 & p in rng c1 )

A349: (X_axis c1) . j1 = (G * (j1,i2)) `1 by A48, A43, A22, A296, GOBOARD1:def 1;

(X_axis c1) . i1 = (G * (i1,i2)) `1 by A49, A43, A22, A298, GOBOARD1:def 1;

hence p `1 <= (G * (i1,i2)) `1 by A49, A52, A43, A22, A333, A342, A346, A344, A348, A343, SEQM_3:def 1; :: thesis: p in rng c1

thus p in rng c1 by A43, A333, A342, A346, A344, A347, PARTFUN2:2; :: thesis: verum

end;then A338: w <= len g2 by A329, A332, XREAL_1:6;

A339: j - (len g1) <> 0 by A336;

then A340: w >= 1 by NAT_1:14;

then A341: w in dom g2 by A338, FINSEQ_3:25;

then reconsider u = i1 - w as Element of NAT by A304, A310;

A342: g /. j = g2 /. w by A340, A337, A338, SEQ_4:136;

A343: u < i1 by A339, XREAL_1:44;

A344: g2 /. w = G * (u,i2) by A309, A310, A341;

A345: (Y_axis c1) . i1 = (G * (i1,i2)) `2 by A49, A43, A21, A298, GOBOARD1:def 2;

A346: i1 - w in dom G by A304, A310, A341;

c1 /. u = c1 . u by A43, A304, A310, A341, PARTFUN1:def 6;

then A347: c1 /. u = G * (u,i2) by A346, MATRIX_0:def 8;

then A348: (X_axis c1) . u = (G * (u,i2)) `1 by A43, A22, A346, GOBOARD1:def 1;

(Y_axis c1) . u = (G * (u,i2)) `2 by A43, A21, A346, A347, GOBOARD1:def 2;

hence p `2 = (G * (i1,i2)) `2 by A49, A53, A43, A21, A333, A342, A346, A344, A345, SEQM_3:def 10; :: thesis: ( (G * (j1,i2)) `1 <= p `1 & p `1 <= (G * (i1,i2)) `1 & p in rng c1 )

A349: (X_axis c1) . j1 = (G * (j1,i2)) `1 by A48, A43, A22, A296, GOBOARD1:def 1;

now :: thesis: (G * (j1,i2)) `1 <= p `1 end;

hence
(G * (j1,i2)) `1 <= p `1
; :: thesis: ( p `1 <= (G * (i1,i2)) `1 & p in rng c1 )(X_axis c1) . i1 = (G * (i1,i2)) `1 by A49, A43, A22, A298, GOBOARD1:def 1;

hence p `1 <= (G * (i1,i2)) `1 by A49, A52, A43, A22, A333, A342, A346, A344, A348, A343, SEQM_3:def 1; :: thesis: p in rng c1

thus p in rng c1 by A43, A333, A342, A346, A344, A347, PARTFUN2:2; :: thesis: verum

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in L~ f or x in L~ g )
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in L~ g or x in L~ f )

assume x in L~ g ; :: thesis: x in L~ f

then consider X being set such that

A351: x in X and

A352: X in { (LSeg (g,i)) where i is Nat : ( 1 <= i & i + 1 <= len g ) } by TARSKI:def 4;

consider i being Nat such that

A353: X = LSeg (g,i) and

A354: 1 <= i and

A355: i + 1 <= len g by A352;

end;assume x in L~ g ; :: thesis: x in L~ f

then consider X being set such that

A351: x in X and

A352: X in { (LSeg (g,i)) where i is Nat : ( 1 <= i & i + 1 <= len g ) } by TARSKI:def 4;

consider i being Nat such that

A353: X = LSeg (g,i) and

A354: 1 <= i and

A355: i + 1 <= len g by A352;

now :: thesis: x in L~ fend;

hence
x in L~ f
; :: thesis: verumper cases
( i + 1 <= len g1 or i + 1 > len g1 )
;

end;

suppose A356:
i + 1 <= len g1
; :: thesis: x in L~ f

i <= i + 1
by NAT_1:11;

then i <= len g1 by A356, XXREAL_0:2;

then A357: i in dom g1 by A354, FINSEQ_3:25;

1 <= i + 1 by NAT_1:11;

then i + 1 in dom g1 by A356, FINSEQ_3:25;

then X = LSeg (g1,i) by A353, A357, TOPREAL3:18;

then X in { (LSeg (g1,j)) where j is Nat : ( 1 <= j & j + 1 <= len g1 ) } by A354, A356;

then A358: x in L~ (f | k) by A36, A351, TARSKI:def 4;

L~ (f | k) c= L~ f by TOPREAL3:20;

hence x in L~ f by A358; :: thesis: verum

end;then i <= len g1 by A356, XXREAL_0:2;

then A357: i in dom g1 by A354, FINSEQ_3:25;

1 <= i + 1 by NAT_1:11;

then i + 1 in dom g1 by A356, FINSEQ_3:25;

then X = LSeg (g1,i) by A353, A357, TOPREAL3:18;

then X in { (LSeg (g1,j)) where j is Nat : ( 1 <= j & j + 1 <= len g1 ) } by A354, A356;

then A358: x in L~ (f | k) by A36, A351, TARSKI:def 4;

L~ (f | k) c= L~ f by TOPREAL3:20;

hence x in L~ f by A358; :: thesis: verum

suppose A359:
i + 1 > len g1
; :: thesis: x in L~ f

reconsider q1 = g /. i, q2 = g /. (i + 1) as Point of (TOP-REAL 2) ;

A360: i <= len g by A355, NAT_1:13;

A361: len g1 <= i by A359, NAT_1:13;

then A362: q1 `2 = (G * (i1,i2)) `2 by A330, A360;

A363: q1 `1 <= (G * (i1,i2)) `1 by A330, A361, A360;

A364: (G * (j1,i2)) `1 <= q1 `1 by A330, A361, A360;

q2 `2 = (G * (i1,i2)) `2 by A330, A355, A359;

then A365: q2 = |[(q2 `1),(q1 `2)]| by A362, EUCLID:53;

A366: q2 `1 <= (G * (i1,i2)) `1 by A330, A355, A359;

A367: ( q1 = |[(q1 `1),(q1 `2)]| & LSeg (g,i) = LSeg (q2,q1) ) by A354, A355, EUCLID:53, TOPREAL1:def 3;

A368: (G * (j1,i2)) `1 <= q2 `1 by A330, A355, A359;

end;A360: i <= len g by A355, NAT_1:13;

A361: len g1 <= i by A359, NAT_1:13;

then A362: q1 `2 = (G * (i1,i2)) `2 by A330, A360;

A363: q1 `1 <= (G * (i1,i2)) `1 by A330, A361, A360;

A364: (G * (j1,i2)) `1 <= q1 `1 by A330, A361, A360;

q2 `2 = (G * (i1,i2)) `2 by A330, A355, A359;

then A365: q2 = |[(q2 `1),(q1 `2)]| by A362, EUCLID:53;

A366: q2 `1 <= (G * (i1,i2)) `1 by A330, A355, A359;

A367: ( q1 = |[(q1 `1),(q1 `2)]| & LSeg (g,i) = LSeg (q2,q1) ) by A354, A355, EUCLID:53, TOPREAL1:def 3;

A368: (G * (j1,i2)) `1 <= q2 `1 by A330, A355, A359;

now :: thesis: x in L~ fend;

hence
x in L~ f
; :: thesis: verumper cases
( q1 `1 > q2 `1 or q1 `1 = q2 `1 or q1 `1 < q2 `1 )
by XXREAL_0:1;

end;

suppose
q1 `1 > q2 `1
; :: thesis: x in L~ f

then
LSeg (g,i) = { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `2 = q1 `2 & q2 `1 <= p2 `1 & p2 `1 <= q1 `1 ) }
by A365, A367, TOPREAL3:10;

then consider p2 being Point of (TOP-REAL 2) such that

A369: ( p2 = x & p2 `2 = q1 `2 ) and

A370: ( q2 `1 <= p2 `1 & p2 `1 <= q1 `1 ) by A351, A353;

( (G * (j1,i2)) `1 <= p2 `1 & p2 `1 <= (G * (i1,i2)) `1 ) by A363, A368, A370, XXREAL_0:2;

then A371: x in LSeg (f,k) by A328, A362, A369;

LSeg (f,k) in { (LSeg (f,j)) where j is Nat : ( 1 <= j & j + 1 <= len f ) } by A3, A13;

hence x in L~ f by A371, TARSKI:def 4; :: thesis: verum

end;then consider p2 being Point of (TOP-REAL 2) such that

A369: ( p2 = x & p2 `2 = q1 `2 ) and

A370: ( q2 `1 <= p2 `1 & p2 `1 <= q1 `1 ) by A351, A353;

( (G * (j1,i2)) `1 <= p2 `1 & p2 `1 <= (G * (i1,i2)) `1 ) by A363, A368, A370, XXREAL_0:2;

then A371: x in LSeg (f,k) by A328, A362, A369;

LSeg (f,k) in { (LSeg (f,j)) where j is Nat : ( 1 <= j & j + 1 <= len f ) } by A3, A13;

hence x in L~ f by A371, TARSKI:def 4; :: thesis: verum

suppose
q1 `1 = q2 `1
; :: thesis: x in L~ f

then
LSeg (g,i) = {q1}
by A365, A367, RLTOPSP1:70;

then x = q1 by A351, A353, TARSKI:def 1;

then A372: x in LSeg (f,k) by A328, A362, A364, A363;

LSeg (f,k) in { (LSeg (f,j)) where j is Nat : ( 1 <= j & j + 1 <= len f ) } by A3, A13;

hence x in L~ f by A372, TARSKI:def 4; :: thesis: verum

end;then x = q1 by A351, A353, TARSKI:def 1;

then A372: x in LSeg (f,k) by A328, A362, A364, A363;

LSeg (f,k) in { (LSeg (f,j)) where j is Nat : ( 1 <= j & j + 1 <= len f ) } by A3, A13;

hence x in L~ f by A372, TARSKI:def 4; :: thesis: verum

suppose
q1 `1 < q2 `1
; :: thesis: x in L~ f

then
LSeg (g,i) = { p1 where p1 is Point of (TOP-REAL 2) : ( p1 `2 = q1 `2 & q1 `1 <= p1 `1 & p1 `1 <= q2 `1 ) }
by A365, A367, TOPREAL3:10;

then consider p2 being Point of (TOP-REAL 2) such that

A373: ( p2 = x & p2 `2 = q1 `2 ) and

A374: ( q1 `1 <= p2 `1 & p2 `1 <= q2 `1 ) by A351, A353;

( (G * (j1,i2)) `1 <= p2 `1 & p2 `1 <= (G * (i1,i2)) `1 ) by A364, A366, A374, XXREAL_0:2;

then A375: x in LSeg (f,k) by A328, A362, A373;

LSeg (f,k) in { (LSeg (f,j)) where j is Nat : ( 1 <= j & j + 1 <= len f ) } by A3, A13;

hence x in L~ f by A375, TARSKI:def 4; :: thesis: verum

end;then consider p2 being Point of (TOP-REAL 2) such that

A373: ( p2 = x & p2 `2 = q1 `2 ) and

A374: ( q1 `1 <= p2 `1 & p2 `1 <= q2 `1 ) by A351, A353;

( (G * (j1,i2)) `1 <= p2 `1 & p2 `1 <= (G * (i1,i2)) `1 ) by A364, A366, A374, XXREAL_0:2;

then A375: x in LSeg (f,k) by A328, A362, A373;

LSeg (f,k) in { (LSeg (f,j)) where j is Nat : ( 1 <= j & j + 1 <= len f ) } by A3, A13;

hence x in L~ f by A375, TARSKI:def 4; :: thesis: verum

assume x in L~ f ; :: thesis: x in L~ g

then A376: x in (L~ (f | k)) \/ (LSeg (f,k)) by A3, A12, Th3;

now :: thesis: x in L~ g

per cases
( x in L~ (f | k) or x in LSeg (f,k) )
by A376, XBOOLE_0:def 3;

suppose
x in LSeg (f,k)
; :: thesis: x in L~ g

then consider p1 being Point of (TOP-REAL 2) such that

A378: p1 = x and

A379: p1 `2 = (G * (i1,i2)) `2 and

A380: (G * (j1,i2)) `1 <= p1 `1 and

A381: p1 `1 <= (G * (i1,i2)) `1 by A328;

defpred S_{3}[ Nat] means ( len g1 <= $1 & $1 <= len g & ( for q being Point of (TOP-REAL 2) st q = g /. $1 holds

q `1 >= p1 `1 ) );

_{3}[n] holds

n <= len g ;

consider ma being Nat such that

A385: ( S_{3}[ma] & ( for n being Nat st S_{3}[n] holds

n <= ma ) ) from NAT_1:sch 6(A384, A382);

reconsider ma = ma as Element of NAT by ORDINAL1:def 12;

A378: p1 = x and

A379: p1 `2 = (G * (i1,i2)) `2 and

A380: (G * (j1,i2)) `1 <= p1 `1 and

A381: p1 `1 <= (G * (i1,i2)) `1 by A328;

defpred S

q `1 >= p1 `1 ) );

A382: now :: thesis: ex n being Nat st S_{3}[n]

A384:
for n being Nat st Sreconsider n = len g1 as Nat ;

take n = n; :: thesis: S_{3}[n]

thus S_{3}[n]
:: thesis: verum

end;take n = n; :: thesis: S

thus S

proof

thus
( len g1 <= n & n <= len g )
by A329, XREAL_1:31; :: thesis: for q being Point of (TOP-REAL 2) st q = g /. n holds

q `1 >= p1 `1

1 <= len g1 by A13, A23, A39, XXREAL_0:2;

then A383: len g1 in dom g1 by FINSEQ_3:25;

let q be Point of (TOP-REAL 2); :: thesis: ( q = g /. n implies q `1 >= p1 `1 )

assume q = g /. n ; :: thesis: q `1 >= p1 `1

then q = (f | k) /. (len (f | k)) by A38, A383, FINSEQ_4:68

.= G * (i1,i2) by A17, A23, A14, A19, FINSEQ_4:71 ;

hence q `1 >= p1 `1 by A381; :: thesis: verum

end;q `1 >= p1 `1

1 <= len g1 by A13, A23, A39, XXREAL_0:2;

then A383: len g1 in dom g1 by FINSEQ_3:25;

let q be Point of (TOP-REAL 2); :: thesis: ( q = g /. n implies q `1 >= p1 `1 )

assume q = g /. n ; :: thesis: q `1 >= p1 `1

then q = (f | k) /. (len (f | k)) by A38, A383, FINSEQ_4:68

.= G * (i1,i2) by A17, A23, A14, A19, FINSEQ_4:71 ;

hence q `1 >= p1 `1 by A381; :: thesis: verum

n <= len g ;

consider ma being Nat such that

A385: ( S

n <= ma ) ) from NAT_1:sch 6(A384, A382);

reconsider ma = ma as Element of NAT by ORDINAL1:def 12;

now :: thesis: x in L~ g

per cases
( ma = len g or ma <> len g )
;

suppose A386:
ma = len g
; :: thesis: x in L~ g

j1 + 1 <= i1
by A295, NAT_1:13;

then A387: 1 <= l by XREAL_1:19;

then 0 + 1 <= ma by A309, A329, A386, XREAL_1:7;

then reconsider m1 = ma - 1 as Element of NAT by INT_1:5;

A388: m1 + 1 = ma ;

(len g1) + 1 <= ma by A309, A329, A386, A387, XREAL_1:7;

then A389: m1 >= len g1 by A388, XREAL_1:6;

reconsider q = g /. m1 as Point of (TOP-REAL 2) ;

set lq = { e where e is Point of (TOP-REAL 2) : ( e `2 = (G * (i1,i2)) `2 & (G * (j1,i2)) `1 <= e `1 & e `1 <= q `1 ) } ;

A390: i1 - l = j1 ;

A391: l in dom g2 by A310, A387, FINSEQ_1:1;

then A392: g /. ma = g2 /. l by A309, A329, A386, FINSEQ_4:69

.= G * (j1,i2) by A309, A310, A391, A390 ;

then p1 `1 <= (G * (j1,i2)) `1 by A385;

then A393: p1 `1 = (G * (j1,i2)) `1 by A380, XXREAL_0:1;

A394: m1 <= len g by A386, A388, NAT_1:11;

then A395: q `2 = (G * (i1,i2)) `2 by A330, A389;

A396: (G * (j1,i2)) `1 <= q `1 by A330, A389, A394;

1 <= len g1 by A13, A23, A39, XXREAL_0:2;

then A397: 1 <= m1 by A389, XXREAL_0:2;

then ( q = |[(q `1),(q `2)]| & LSeg (g,m1) = LSeg ((G * (j1,i2)),q) ) by A386, A392, A388, EUCLID:53, TOPREAL1:def 3;

then LSeg (g,m1) = { e where e is Point of (TOP-REAL 2) : ( e `2 = (G * (i1,i2)) `2 & (G * (j1,i2)) `1 <= e `1 & e `1 <= q `1 ) } by A302, A327, A395, A396, TOPREAL3:10;

then A398: p1 in LSeg (g,m1) by A379, A393, A396;

LSeg (g,m1) in { (LSeg (g,i)) where i is Nat : ( 1 <= i & i + 1 <= len g ) } by A386, A388, A397;

hence x in L~

then A387: 1 <= l by XREAL_1:19;

then 0 + 1 <= ma by A309, A329, A386, XREAL_1:7;

then reconsider m1 = ma - 1 as Element of NAT by INT_1:5;

A388: m1 + 1 = ma ;

(len g1) + 1 <= ma by A309, A329, A386, A387, XREAL_1:7;

then A389: m1 >= len g1 by A388, XREAL_1:6;

reconsider q = g /. m1 as Point of (TOP-REAL 2) ;

set lq = { e where e is Point of (TOP-REAL 2) : ( e `2 = (G * (i1,i2)) `2 & (G * (j1,i2)) `1 <= e `1 & e `1 <= q `1 ) } ;

A390: i1 - l = j1 ;

A391: l in dom g2 by A310, A387, FINSEQ_1:1;

then A392: g /. ma = g2 /. l by A309, A329, A386, FINSEQ_4:69

.= G * (j1,i2) by A309, A310, A391, A390 ;

then p1 `1 <= (G * (j1,i2)) `1 by A385;

then A393: p1 `1 = (G * (j1,i2)) `1 by A380, XXREAL_0:1;

A394: m1 <= len g by A386, A388, NAT_1:11;

then A395: q `2 = (G * (i1,i2)) `2 by A330, A389;

A396: (G * (j1,i2)) `1 <= q `1 by A330, A389, A394;

1 <= len g1 by A13, A23, A39, XXREAL_0:2;

then A397: 1 <= m1 by A389, XXREAL_0:2;

then ( q = |[(q `1),(q `2)]| & LSeg (g,m1) = LSeg ((G * (j1,i2)),q) ) by A386, A392, A388, EUCLID:53, TOPREAL1:def 3;

then LSeg (g,m1) = { e where e is Point of (TOP-REAL 2) : ( e `2 = (G * (i1,i2)) `2 & (G * (j1,i2)) `1 <= e `1 & e `1 <= q `1 ) } by A302, A327, A395, A396, TOPREAL3:10;

then A398: p1 in LSeg (g,m1) by A379, A393, A396;

LSeg (g,m1) in { (LSeg (g,i)) where i is Nat : ( 1 <= i & i + 1 <= len g ) } by A386, A388, A397;

hence x in L~