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₁[ 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₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A2: S₁[k] ; :: thesis: S₁[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;

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 )

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 )

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;

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

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;

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 )
thus ( L~ f = L~ g & g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g ) ; :: thesis: verum

end;

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 )

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;

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) )

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;

A28: f | k is special

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;

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)

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;

then consider g1 being FinSequence of (TOP-REAL 2) such that
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 )

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 )

set ppi = G * (i1,i2);
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 ) ) )

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

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 )

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₂[ 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;

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) )

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;

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₂[n,p]

let n be Nat; :: thesis: ( n in Seg l implies ex p being Element of the carrier of (TOP-REAL 2) st S₂[n,p] )
assume n in Seg l ; :: thesis: ex p being Element of the carrier of (TOP-REAL 2) st S₂[n,p]
then reconsider m = i2 - n as Element of NAT by A68;
take p = G * (i1,m); :: thesis: S₂[n,p]
thus S₂[n,p] ; :: thesis: verum

end;

consider g2 being FinSequence of (TOP-REAL 2) such that
A73: ( len g2 = l & ( for n being Nat st n in Seg l holds
S₂[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;

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

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;

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) )

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;

then A84: for n being Nat st n in dom g holds
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

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;

then for n being Nat st n in dom g & n + 1 in dom g holds
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

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;

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 )

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;

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

per cases ( j = len g1 or j <> len g1 ) ;

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;

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;

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

per cases ( u = j2 or u <> j2 ) ;

suppose u = j2 ; :: thesis: (G * (i1,j2)) `2 <= p `2

hence (G * (i1,j2)) `2 <= p `2 by A97, A105, A102, A103, A110, SEQ_4:136; :: thesis: verum

end;

suppose A115: u <> j2 ; :: thesis: (G * (i1,j2)) `2 <= p `2

i2 - (len g2) <= u by A103, XREAL_1:13;
then j2 < u by A73, A115, XXREAL_0:1;
hence (G * (i1,j2)) `2 <= p `2 by A56, A54, A20, A55, A97, A107, A111, A110, A113, A114, SEQM_3:def 1; :: thesis: verum

end;

end;

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

end;

end;

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

end;

thus L~ g c= L~ f :: according to XBOOLE_0:def 10 :: thesis: L~ f c= L~ g

proof

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;

now :: thesis: x in L~ f

per cases ( i + 1 <= len g1 or i + 1 > len g1 ) ;

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;

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;

now :: thesis: x in L~ f

per cases ( q1 `2 > q2 `2 or q1 `2 = q2 `2 or q1 `2 < q2 `2 ) by XXREAL_0:1;

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;

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;

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;

end;

end;

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

end;

end;

end;

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

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in L~ f or x in L~ g )
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~ g

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

suppose A142: x in L~ (f | k) ; :: thesis: x in L~ g

L~ g1 c= L~ g by Th6;
hence x in L~ g by A36, A142; :: thesis: verum

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₃[ 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 ) );

A147: now :: thesis: ex n being Nat st S₃[n]

reconsider n = len g1 as Nat ;
take n = n; :: thesis: S₃[n]
thus S₃[n] :: thesis: verum

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;

end;

A149: for n being Nat st S₃[n] holds
n <= len g ;
consider ma being Nat such that
A150: ( S₃[ma] & ( for n being Nat st S₃[n] holds
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~ g

per cases ( ma = len g or ma <> len g ) ;

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;

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;

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

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;

A170: ( qa `1 = (G * (i1,i2)) `1 & qa = |[(qa `1),(qa `2)]| ) by A94, A150, EUCLID:53;
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;

end;

end;

hence x in L~ g ; :: thesis: verum

end;

end;

end;

hence x in L~ g ; :: thesis: verum

end;

1 <= len g1 by A13, A23, A39, XXREAL_0:2;
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;

case i2 = j2 ; :: thesis: contradiction

hence contradiction by A6, A17, A19, A44, A46, A58; :: thesis: verum

end;

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 )

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₁( 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₁(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 )

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 )

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;

A184: dom g2 = Seg (len g2) by FINSEQ_1:def 3;

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) )

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;

then A186: for n being Nat st n in dom g holds
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

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;

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

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;

then for n being Nat st n in dom g & n + 1 in dom g holds
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

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;

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 )

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;

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

per cases ( j = len g1 or j <> len g1 ) ;

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;

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;

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

per cases ( i2 + w = j2 or i2 + w <> j2 ) ;

suppose i2 + w = j2 ; :: thesis: p `2 <= (G * (i1,j2)) `2

hence p `2 <= (G * (i1,j2)) `2 by A215, A224, A220, A221, A231, SEQ_4:136; :: thesis: verum

end;

suppose A233: i2 + w <> j2 ; :: thesis: p `2 <= (G * (i1,j2)) `2

i2 + w <= i2 + l by A178, A221, XREAL_1:7;
then i2 + w < j2 by A233, XXREAL_0:1;
hence p `2 <= (G * (i1,j2)) `2 by A56, A54, A20, A55, A215, A225, A231, A228, A230, A232, SEQM_3:def 1; :: thesis: verum

end;

end;

end;

hence p `2 <= (G * (i1,j2)) `2 ; :: thesis: p in rng l1
thus p in rng l1 by A55, A215, A216, A225, A231, A228, A229, PARTFUN2:2; :: thesis: verum

end;

end;

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

end;

thus L~ g c= L~ f :: according to XBOOLE_0:def 10 :: thesis: L~ f c= L~ g

proof

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;

now :: thesis: x in L~ f

per cases ( i + 1 <= len g1 or i + 1 > len g1 ) ;

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;

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;

now :: thesis: x in L~ f

per cases ( q1 `2 > q2 `2 or q1 `2 = q2 `2 or q1 `2 < q2 `2 ) by XXREAL_0:1;

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;

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;

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;

end;

end;

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

end;

end;

end;

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

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in L~ f or x in L~ g )
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~ g

per cases ( x in L~ (f | k) or x in LSeg (f,k) ) by A259, XBOOLE_0:def 3;

suppose A260: x in L~ (f | k) ; :: thesis: x in L~ g

L~ g1 c= L~ g by Th6;
hence x in L~ g by A36, A260; :: thesis: verum

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₂[ 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 ) );

A265: now :: thesis: ex n being Nat st S₂[n]

reconsider n = len g1 as Nat ;
take n = n; :: thesis: S₂[n]
thus S₂[n] :: thesis: verum

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;

end;

A267: for n being Nat st S₂[n] holds
n <= len g ;
consider ma being Nat such that
A268: ( S₂[ma] & ( for n being Nat st S₂[n] holds
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~ g

per cases ( ma = len g or ma <> len g ) ;

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;

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;

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

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;

A288: ( qa `1 = (G * (i1,i2)) `1 & qa = |[(qa `1),(qa `2)]| ) by A212, A268, EUCLID:53;
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;

end;

end;

hence x in L~ g ; :: thesis: verum

end;

end;

end;

hence x in L~ g ; :: thesis: verum

end;

1 <= len g1 by A13, A23, A39, XXREAL_0:2;
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;

end;

end;

hence 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 ) ; :: thesis: verum

end;

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 )

set ppi = G * (i1,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 ) ) )

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 )

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₂[ 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;

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 )

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;

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₂[n,p]

let n be Nat; :: thesis: ( n in Seg l implies ex p being Element of the carrier of (TOP-REAL 2) st S₂[n,p] )
assume n in Seg l ; :: thesis: ex p being Element of the carrier of (TOP-REAL 2) st S₂[n,p]
then reconsider m = i1 - n as Element of NAT by A304;
take p = G * (m,i2); :: thesis: S₂[n,p]
thus S₂[n,p] ; :: thesis: verum

end;

consider g2 being FinSequence of (TOP-REAL 2) such that
A309: ( len g2 = l & ( for n being Nat st n in Seg l holds
S₂[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;

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

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;

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) )

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;

then A320: for n being Nat st n in dom g holds
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

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;

then for n being Nat st n in dom g & n + 1 in dom g holds
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;

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 )

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 )

now :: thesis: ( p `2 = (G * (i1,i2)) `2 & (G * (j1,i2)) `1 <= p `1 & p `1 <= (G * (i1,i2)) `1 & p in rng c1 )

per cases ( j = len g1 or j <> len g1 ) ;

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;

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;

now :: thesis: (G * (j1,i2)) `1 <= p `1

per cases ( u = j1 or u <> j1 ) ;

suppose u = j1 ; :: thesis: (G * (j1,i2)) `1 <= p `1

hence (G * (j1,i2)) `1 <= p `1 by A333, A340, A337, A338, A344, SEQ_4:136; :: thesis: verum

end;

suppose A350: u <> j1 ; :: thesis: (G * (j1,i2)) `1 <= p `1

i1 - (len g2) <= u by A338, XREAL_1:13;
then j1 < u by A309, A350, XXREAL_0:1;
hence (G * (j1,i2)) `1 <= p `1 by A48, A52, A43, A22, A333, A342, A346, A344, A348, A349, SEQM_3:def 1; :: thesis: verum

end;

end;

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

end;

end;

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

end;

thus L~ g c= L~ f :: according to XBOOLE_0:def 10 :: thesis: L~ f c= L~ g

proof

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;

now :: thesis: x in L~ f

per cases ( i + 1 <= len g1 or i + 1 > len g1 ) ;

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;

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;

now :: thesis: x in L~ f

per cases ( q1 `1 > q2 `1 or q1 `1 = q2 `1 or q1 `1 < q2 `1 ) by XXREAL_0:1;

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;

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;

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;

end;

end;

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

end;

end;

end;

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

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in L~ f or x in L~ g )
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 A377: x in L~ (f | k) ; :: thesis: x in L~ g

L~ g1 c= L~ g by Th6;
hence x in L~ g by A36, A377; :: thesis: verum

end;

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₃[ 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 ) );

A382: now :: thesis: ex n being Nat st S₃[n]

reconsider n = len g1 as Nat ;
take n = n; :: thesis: S₃[n]
thus S₃[n] :: thesis: verum

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;

end;

A384: for n being Nat st S₃[n] holds
n <= len g ;
consider ma being Nat such that
A385: ( S₃[ma] & ( for n being Nat st S₃[n] holds
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~ g by A378, A398, TARSKI:def 4; :: thesis: verum

end;

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

then ma < len g by A385, XXREAL_0:1;
then A399: 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 `2 = (G * (i1,i2)) `2 & qa1 `1 <= p2 `1 & p2 `1 <= qa `1 ) } ;
A400: qa1 = |[(qa1 `1),(qa1 `2)]| by EUCLID:53;
A401: p1 `1 <= qa `1 by A385;
A402: len g1 <= ma + 1 by A385, NAT_1:13;
then A403: qa1 `2 = (G * (i1,i2)) `2 by A330, A399;

A404: now :: thesis: not p1 `1 <= qa1 `1

assume p1 `1 <= qa1 `1 ; :: thesis: contradiction
then for q being Point of (TOP-REAL 2) st q = g /. (ma + 1) holds
p1 `1 <= q `1 ;
then ma + 1 <= ma by A385, A399, A402;
hence contradiction by XREAL_1:29; :: thesis: verum

end;

A405: ( qa `2 = (G * (i1,i2)) `2 & qa = |[(qa `1),(qa `2)]| ) by A330, A385, EUCLID:53;
A406: 1 <= ma by A13, A23, A39, A385, NAT_1:13;
then LSeg (g,ma) = LSeg (qa1,qa) by A399, TOPREAL1:def 3
.= { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `2 = (G * (i1,i2)) `2 & qa1 `1 <= p2 `1 & p2 `1 <= qa `1 ) } by A401, A404, A403, A405, A400, TOPREAL3:10, XXREAL_0:2 ;
then A407: x in LSeg (g,ma) by A378, A379, A401, A404;
LSeg (g,ma) in { (LSeg (g,i)) where i is Nat : ( 1 <= i & i + 1 <= len g ) } by A406, A399;
hence x in L~ g by A407, TARSKI:def 4; :: thesis: verum

end;

end;

end;

hence x in L~ g ; :: thesis: verum

end;

end;

end;

hence x in L~ g ; :: thesis: verum

end;

1 <= len g1 by A13, A23, A39, XXREAL_0:2;
then 1 in dom g1 by A57, FINSEQ_1:1;
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 )
A408: len g = (len g1) + (len g2) by FINSEQ_1:22;
j1 + 1 <= i1 by A295, NAT_1:13;
then A409: 1 <= l by XREAL_1:19;
then A410: l in dom g2 by A310, FINSEQ_1:1;
hence g /. (len g) = g2 /. l by A309, A408, FINSEQ_4:69
.= G * (m1,i2) by A309, A310, A410
.= f /. (len f) by A3, A46, A294 ;
:: thesis: len f <= len g
thus len f <= len g by A3, A23, A39, A309, A409, A408, XREAL_1:7; :: thesis: verum

end;

case i1 = j1 ; :: thesis: contradiction

hence contradiction by A6, A17, A19, A44, A46, A294; :: thesis: verum

end;

case A411: 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 )

set lk = { w where w is Point of (TOP-REAL 2) : ( w `2 = (G * (i1,i2)) `2 & (G * (i1,i2)) `1 <= w `1 & w `1 <= (G * (j1,i2)) `1 ) } ;
A412: G * (i1,i2) = |[((G * (i1,i2)) `1),((G * (i1,i2)) `2)]| by EUCLID:53;
reconsider l = j1 - i1 as Element of NAT by A411, INT_1:5;
deffunc H₁( Nat) -> Element of the carrier of (TOP-REAL 2) = G * ((i1 + $1),i2);
consider g2 being FinSequence of (TOP-REAL 2) such that
A413: ( len g2 = l & ( for n being Nat st n in dom g2 holds
g2 /. n = H₁(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 )

A414: now :: thesis: for n being Nat st n in Seg l holds
( i1 + n in dom G & [(i1 + n),i2] in Indices G )

let n be Nat; :: thesis: ( n in Seg l implies ( i1 + n in dom G & [(i1 + n),i2] in Indices G ) )
A415: n <= i1 + n by NAT_1:11;
assume A416: n in Seg l ; :: thesis: ( i1 + n in dom G & [(i1 + n),i2] in Indices G )
then n <= l by FINSEQ_1:1;
then A417: i1 + n <= l + i1 by XREAL_1:7;
j1 <= len G by A48, FINSEQ_3:25;
then A418: i1 + n <= len G by A417, XXREAL_0:2;
1 <= n by A416, FINSEQ_1:1;
then 1 <= i1 + n by A415, XXREAL_0:2;
hence i1 + n in dom G by A418, FINSEQ_3:25; :: thesis: [(i1 + n),i2] in Indices G
hence [(i1 + n),i2] in Indices G by A47, A51, ZFMISC_1:87; :: thesis: verum

end;

A419: dom g2 = Seg (len g2) by FINSEQ_1:def 3;

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) )

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 A420: n in dom g2 ; :: thesis: ex m, k being Nat st
( [m,k] in Indices G & g2 /. n = G * (m,k) )
reconsider m = i1 + n, 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 A413, A414, A419, A420; :: thesis: verum

end;

then A421: for n being Nat st n in dom g holds
ex i, j being Nat st
( [i,j] in Indices G & g /. n = G * (i,j) ) by A40, GOBOARD1:23;

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

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
A423: n in dom g2 and
A424: 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
A425: [l1,l2] in Indices G and
A426: [l3,l4] in Indices G and
A427: g2 /. n = G * (l1,l2) and
A428: g2 /. (n + 1) = G * (l3,l4) ; :: thesis: |.(l1 - l3).| + |.(l2 - l4).| = 1
( g2 /. (n + 1) = G * ((i1 + (n + 1)),i2) & [(i1 + (n + 1)),i2] in Indices G ) by A413, A414, A419, A424;
then A429: ( l3 = i1 + (n + 1) & l4 = i2 ) by A426, A428, GOBOARD1:5;
( g2 /. n = G * ((i1 + n),i2) & [(i1 + n),i2] in Indices G ) by A413, A414, A419, A423;
then ( l1 = i1 + n & l2 = i2 ) by A425, A427, GOBOARD1:5;
hence |.(l1 - l3).| + |.(l2 - l4).| = |.((i1 + n) - (i1 + (n + 1))).| + 0 by A429, ABSVALUE:2
.= |.(- 1).|
.= |.1.| by COMPLEX1:52
.= 1 by ABSVALUE:def 1 ;
:: thesis: verum

end;

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

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
A430: [l1,l2] in Indices G and
A431: [l3,l4] in Indices G and
A432: g1 /. (len g1) = G * (l1,l2) and
A433: g2 /. 1 = G * (l3,l4) and
len g1 in dom g1 and
A434: 1 in dom g2 ; :: thesis: |.(l1 - l3).| + |.(l2 - l4).| = 1
( g2 /. 1 = G * ((i1 + 1),i2) & [(i1 + 1),i2] in Indices G ) by A413, A414, A419, A434;
then A435: ( l3 = i1 + 1 & l4 = i2 ) by A431, A433, 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, A430, A432, GOBOARD1:5;
hence |.(l1 - l3).| + |.(l2 - l4).| = |.(i1 - (i1 + 1)).| + 0 by A435, ABSVALUE:2
.= |.((i1 - i1) + (- 1)).|
.= |.1.| by COMPLEX1:52
.= 1 by ABSVALUE:def 1 ;
:: thesis: verum

end;

then for n being Nat st n in dom g & n + 1 in dom g holds
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, A422, GOBOARD1:24;
hence g is_sequence_on G by A421; :: thesis: ( L~ g = L~ f & g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g )
A436: G * (j1,i2) = |[((G * (j1,i2)) `1),((G * (j1,i2)) `2)]| by EUCLID:53;
c1 /. j1 = c1 . j1 by A48, A43, PARTFUN1:def 6;
then A437: c1 /. j1 = G * (j1,i2) by A48, MATRIX_0:def 8;
then A438: (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 A439: c1 /. i1 = G * (i1,i2) by A49, MATRIX_0:def 8;
then A440: (X_axis c1) . i1 = (G * (i1,i2)) `1 by A49, A43, A22, GOBOARD1:def 1;
then A441: (G * (i1,i2)) `1 < (G * (j1,i2)) `1 by A49, A48, A52, A43, A22, A411, A438, SEQM_3:def 1;
A442: (Y_axis c1) . j1 = (G * (j1,i2)) `2 by A48, A43, A21, A437, GOBOARD1:def 2;
(Y_axis c1) . i1 = (G * (i1,i2)) `2 by A49, A43, A21, A439, GOBOARD1:def 2;
then A443: (G * (i1,i2)) `2 = (G * (j1,i2)) `2 by A49, A48, A53, A43, A21, A442, SEQM_3:def 10;
A444: LSeg (f,k) = LSeg ((G * (i1,i2)),(G * (j1,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 * (i1,i2)) `1 <= w `1 & w `1 <= (G * (j1,i2)) `1 ) } by A441, A443, A412, A436, TOPREAL3:10 ;
A445: dom g2 = Seg l by A413, 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

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 ) } ;
A446: len g = (len g1) + (len g2) by FINSEQ_1:22;

A447: 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 * (i1,i2)) `1 <= p `1 & p `1 <= (G * (j1,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 * (i1,i2)) `1 <= p `1 & p `1 <= (G * (j1,i2)) `1 & p in rng c1 ) )
assume that
A448: len g1 <= j and
A449: j <= len g ; :: thesis: for p being Point of (TOP-REAL 2) st p = g /. j holds
( p `2 = (G * (i1,i2)) `2 & (G * (i1,i2)) `1 <= p `1 & p `1 <= (G * (j1,i2)) `1 & p in rng c1 )
reconsider w = j - (len g1) as Element of NAT by A448, INT_1:5;
set u = i1 + w;
let p be Point of (TOP-REAL 2); :: thesis: ( p = g /. j implies ( p `2 = (G * (i1,i2)) `2 & (G * (i1,i2)) `1 <= p `1 & p `1 <= (G * (j1,i2)) `1 & p in rng c1 ) )
assume A450: p = g /. j ; :: thesis: ( p `2 = (G * (i1,i2)) `2 & (G * (i1,i2)) `1 <= p `1 & p `1 <= (G * (j1,i2)) `1 & p in rng c1 )

now :: thesis: ( p `2 = (G * (i1,i2)) `2 & (G * (i1,i2)) `1 <= p `1 & p `1 <= (G * (j1,i2)) `1 & p in rng c1 )

per cases ( j = len g1 or j <> len g1 ) ;

suppose A451: j = len g1 ; :: thesis: ( p `2 = (G * (i1,i2)) `2 & (G * (i1,i2)) `1 <= p `1 & p `1 <= (G * (j1,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 A452: 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 A450, A451; :: thesis: ( (G * (i1,i2)) `1 <= p `1 & p `1 <= (G * (j1,i2)) `1 & p in rng c1 )
thus ( (G * (i1,i2)) `1 <= p `1 & p `1 <= (G * (j1,i2)) `1 ) by A49, A48, A52, A43, A22, A411, A440, A438, A450, A451, A452, SEQM_3:def 1; :: thesis: p in rng c1
thus p in rng c1 by A49, A43, A439, A450, A451, A452, PARTFUN2:2; :: thesis: verum

end;

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

A454: w + (len g1) = j ;
then A455: w <= len g2 by A446, A449, XREAL_1:6;
A456: (Y_axis c1) . i1 = (G * (i1,i2)) `2 by A49, A43, A21, A439, GOBOARD1:def 2;
A457: j - (len g1) <> 0 by A453;
then A458: w >= 1 by NAT_1:14;
then A459: g /. j = g2 /. w by A454, A455, SEQ_4:136;
A460: i1 < i1 + w by A457, XREAL_1:29;
A461: w in dom g2 by A458, A455, FINSEQ_3:25;
then A462: i1 + w in dom G by A445, A414;
c1 /. (i1 + w) = c1 . (i1 + w) by A43, A445, A414, A461, PARTFUN1:def 6;
then A463: c1 /. (i1 + w) = G * ((i1 + w),i2) by A462, MATRIX_0:def 8;
then A464: (X_axis c1) . (i1 + w) = (G * ((i1 + w),i2)) `1 by A43, A22, A462, GOBOARD1:def 1;
A465: g2 /. w = G * ((i1 + w),i2) by A413, A461;
(Y_axis c1) . (i1 + w) = (G * ((i1 + w),i2)) `2 by A43, A21, A462, A463, GOBOARD1:def 2;
hence p `2 = (G * (i1,i2)) `2 by A49, A53, A43, A21, A450, A459, A465, A462, A456, SEQM_3:def 10; :: thesis: ( (G * (i1,i2)) `1 <= p `1 & p `1 <= (G * (j1,i2)) `1 & p in rng c1 )
(X_axis c1) . i1 = (G * (i1,i2)) `1 by A49, A43, A22, A439, GOBOARD1:def 1;
hence (G * (i1,i2)) `1 <= p `1 by A49, A52, A43, A22, A450, A459, A465, A462, A464, A460, SEQM_3:def 1; :: thesis: ( p `1 <= (G * (j1,i2)) `1 & p in rng c1 )
A466: (X_axis c1) . j1 = (G * (j1,i2)) `1 by A48, A43, A22, A437, GOBOARD1:def 1;

now :: thesis: p `1 <= (G * (j1,i2)) `1

per cases ( i1 + w = j1 or i1 + w <> j1 ) ;

suppose i1 + w = j1 ; :: thesis: p `1 <= (G * (j1,i2)) `1

hence p `1 <= (G * (j1,i2)) `1 by A450, A458, A454, A455, A465, SEQ_4:136; :: thesis: verum

end;

suppose A467: i1 + w <> j1 ; :: thesis: p `1 <= (G * (j1,i2)) `1

i1 + w <= i1 + l by A413, A455, XREAL_1:7;
then i1 + w < j1 by A467, XXREAL_0:1;
hence p `1 <= (G * (j1,i2)) `1 by A48, A52, A43, A22, A450, A459, A465, A462, A464, A466, SEQM_3:def 1; :: thesis: verum

end;

end;

end;

hence p `1 <= (G * (j1,i2)) `1 ; :: thesis: p in rng c1
thus p in rng c1 by A43, A450, A459, A465, A462, A463, PARTFUN2:2; :: thesis: verum

end;

end;

end;

hence ( p `2 = (G * (i1,i2)) `2 & (G * (i1,i2)) `1 <= p `1 & p `1 <= (G * (j1,i2)) `1 & p in rng c1 ) ; :: thesis: verum

end;

thus L~ g c= L~ f :: according to XBOOLE_0:def 10 :: thesis: L~ f c= L~ g

proof

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
A468: x in X and
A469: 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
A470: X = LSeg (g,i) and
A471: 1 <= i and
A472: i + 1 <= len g by A469;

now :: thesis: x in L~ f

per cases ( i + 1 <= len g1 or i + 1 > len g1 ) ;

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

i <= i + 1 by NAT_1:11;
then i <= len g1 by A473, XXREAL_0:2;
then A474: i in dom g1 by A471, FINSEQ_3:25;
1 <= i + 1 by NAT_1:11;
then i + 1 in dom g1 by A473, FINSEQ_3:25;
then X = LSeg (g1,i) by A470, A474, TOPREAL3:18;
then X in { (LSeg (g1,j)) where j is Nat : ( 1 <= j & j + 1 <= len g1 ) } by A471, A473;
then A475: x in L~ (f | k) by A36, A468, TARSKI:def 4;
L~ (f | k) c= L~ f by TOPREAL3:20;
hence x in L~ f by A475; :: thesis: verum

end;

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

reconsider q1 = g /. i, q2 = g /. (i + 1) as Point of (TOP-REAL 2) ;
A477: i <= len g by A472, NAT_1:13;
A478: len g1 <= i by A476, NAT_1:13;
then A479: q1 `2 = (G * (i1,i2)) `2 by A447, A477;
A480: q1 `1 <= (G * (j1,i2)) `1 by A447, A478, A477;
A481: (G * (i1,i2)) `1 <= q1 `1 by A447, A478, A477;
q2 `2 = (G * (i1,i2)) `2 by A447, A472, A476;
then A482: q2 = |[(q2 `1),(q1 `2)]| by A479, EUCLID:53;
A483: q2 `1 <= (G * (j1,i2)) `1 by A447, A472, A476;
A484: ( q1 = |[(q1 `1),(q1 `2)]| & LSeg (g,i) = LSeg (q2,q1) ) by A471, A472, EUCLID:53, TOPREAL1:def 3;
A485: (G * (i1,i2)) `1 <= q2 `1 by A447, A472, A476;

now :: thesis: x in L~ f

per cases ( q1 `1 > q2 `1 or q1 `1 = q2 `1 or q1 `1 < q2 `1 ) by XXREAL_0:1;

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 A482, A484, TOPREAL3:10;
then consider p2 being Point of (TOP-REAL 2) such that
A486: ( p2 = x & p2 `2 = q1 `2 ) and
A487: ( q2 `1 <= p2 `1 & p2 `1 <= q1 `1 ) by A468, A470;
( (G * (i1,i2)) `1 <= p2 `1 & p2 `1 <= (G * (j1,i2)) `1 ) by A480, A485, A487, XXREAL_0:2;
then A488: x in LSeg (f,k) by A444, A479, A486;
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 A488, TARSKI:def 4; :: thesis: verum

end;

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

then LSeg (g,i) = {q1} by A482, A484, RLTOPSP1:70;
then x = q1 by A468, A470, TARSKI:def 1;
then A489: x in LSeg (f,k) by A444, A479, A481, A480;
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 A489, TARSKI:def 4; :: thesis: verum

end;

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 A482, A484, TOPREAL3:10;
then consider p2 being Point of (TOP-REAL 2) such that
A490: ( p2 = x & p2 `2 = q1 `2 ) and
A491: ( q1 `1 <= p2 `1 & p2 `1 <= q2 `1 ) by A468, A470;
( (G * (i1,i2)) `1 <= p2 `1 & p2 `1 <= (G * (j1,i2)) `1 ) by A481, A483, A491, XXREAL_0:2;
then A492: x in LSeg (f,k) by A444, A479, A490;
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 A492, TARSKI:def 4; :: thesis: verum

end;

end;

end;

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

end;

end;

end;

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

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in L~ f or x in L~ g )
assume x in L~ f ; :: thesis: x in L~ g
then A493: 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 A493, XBOOLE_0:def 3;

suppose A494: x in L~ (f | k) ; :: thesis: x in L~ g

L~ g1 c= L~ g by Th6;
hence x in L~ g by A36, A494; :: thesis: verum

end;

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

then consider p1 being Point of (TOP-REAL 2) such that
A495: p1 = x and
A496: p1 `2 = (G * (i1,i2)) `2 and
A497: (G * (i1,i2)) `1 <= p1 `1 and
A498: p1 `1 <= (G * (j1,i2)) `1 by A444;
defpred S₂[ 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 ) );

A499: now :: thesis: ex n being Nat st S₂[n]

reconsider n = len g1 as Nat ;
take n = n; :: thesis: S₂[n]
thus S₂[n] :: thesis: verum

proof

thus ( len g1 <= n & n <= len g ) by A446, 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 A500: 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, A500, FINSEQ_4:68
.= G * (i1,i2) by A17, A23, A14, A19, FINSEQ_4:71 ;
hence q `1 <= p1 `1 by A497; :: thesis: verum

end;

end;

A501: for n being Nat st S₂[n] holds
n <= len g ;
consider ma being Nat such that
A502: ( S₂[ma] & ( for n being Nat st S₂[n] holds
n <= ma ) ) from NAT_1:sch 6(A501, A499);
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 A503: ma = len g ; :: thesis: x in L~ g

i1 + 1 <= j1 by A411, NAT_1:13;
then A504: 1 <= l by XREAL_1:19;
then 0 + 1 <= ma by A413, A446, A503, XREAL_1:7;
then reconsider m1 = ma - 1 as Element of NAT by INT_1:5;
A505: m1 + 1 = ma ;
(len g1) + 1 <= ma by A413, A446, A503, A504, XREAL_1:7;
then A506: m1 >= len g1 by A505, 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 & q `1 <= e `1 & e `1 <= (G * (j1,i2)) `1 ) } ;
A507: i1 + l = j1 ;
A508: l in dom g2 by A413, A504, FINSEQ_3:25;
then A509: g /. ma = g2 /. l by A413, A446, A503, FINSEQ_4:69
.= G * (j1,i2) by A413, A508, A507 ;
then (G * (j1,i2)) `1 <= p1 `1 by A502;
then A510: p1 `1 = (G * (j1,i2)) `1 by A498, XXREAL_0:1;
A511: m1 <= len g by A503, A505, NAT_1:11;
then A512: q `2 = (G * (i1,i2)) `2 by A447, A506;
A513: q `1 <= (G * (j1,i2)) `1 by A447, A506, A511;
1 <= len g1 by A13, A23, A39, XXREAL_0:2;
then A514: 1 <= m1 by A506, XXREAL_0:2;
then ( q = |[(q `1),(q `2)]| & LSeg (g,m1) = LSeg ((G * (j1,i2)),q) ) by A503, A509, A505, EUCLID:53, TOPREAL1:def 3;
then LSeg (g,m1) = { e where e is Point of (TOP-REAL 2) : ( e `2 = (G * (i1,i2)) `2 & q `1 <= e `1 & e `1 <= (G * (j1,i2)) `1 ) } by A443, A436, A512, A513, TOPREAL3:10;
then A515: p1 in LSeg (g,m1) by A496, A510, A513;
LSeg (g,m1) in { (LSeg (g,i)) where i is Nat : ( 1 <= i & i + 1 <= len g ) } by A503, A505, A514;
hence x in L~ g by A495, A515, TARSKI:def 4; :: thesis: verum

end;

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

then ma < len g by A502, XXREAL_0:1;
then A516: 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 `2 = (G * (i1,i2)) `2 & qa `1 <= p2 `1 & p2 `1 <= qa1 `1 ) } ;
A517: qa1 = |[(qa1 `1),(qa1 `2)]| by EUCLID:53;
A518: qa `1 <= p1 `1 by A502;
A519: len g1 <= ma + 1 by A502, NAT_1:13;
then A520: qa1 `2 = (G * (i1,i2)) `2 by A447, A516;

A521: now :: thesis: not qa1 `1 <= p1 `1

assume qa1 `1 <= p1 `1 ; :: thesis: contradiction
then for q being Point of (TOP-REAL 2) st q = g /. (ma + 1) holds
q `1 <= p1 `1 ;
then ma + 1 <= ma by A502, A516, A519;
hence contradiction by XREAL_1:29; :: thesis: verum

end;

A522: ( qa `2 = (G * (i1,i2)) `2 & qa = |[(qa `1),(qa `2)]| ) by A447, A502, EUCLID:53;
A523: 1 <= ma by A13, A23, A39, A502, NAT_1:13;
then LSeg (g,ma) = LSeg (qa,qa1) by A516, TOPREAL1:def 3
.= { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `2 = (G * (i1,i2)) `2 & qa `1 <= p2 `1 & p2 `1 <= qa1 `1 ) } by A518, A521, A520, A522, A517, TOPREAL3:10, XXREAL_0:2 ;
then A524: x in LSeg (g,ma) by A495, A496, A518, A521;
LSeg (g,ma) in { (LSeg (g,i)) where i is Nat : ( 1 <= i & i + 1 <= len g ) } by A523, A516;
hence x in L~ g by A524, TARSKI:def 4; :: thesis: verum

end;

end;

end;

hence x in L~ g ; :: thesis: verum

end;

end;

end;

hence x in L~ g ; :: thesis: verum

end;

1 <= len g1 by A13, A23, A39, XXREAL_0:2;
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 )
A525: len g = (len g1) + l by A413, FINSEQ_1:22;
i1 + 1 <= j1 by A411, NAT_1:13;
then A526: 1 <= l by XREAL_1:19;
then A527: l in dom g2 by A413, A419, FINSEQ_1:1;
hence g /. (len g) = g2 /. l by A525, FINSEQ_4:69
.= G * ((i1 + l),i2) by A413, A527
.= f /. (len f) by A3, A46, A294 ;
:: thesis: len f <= len g
thus len f <= len g by A3, A23, A39, A526, A525, XREAL_1:7; :: thesis: verum

end;

end;

end;

hence 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 ) ; :: thesis: verum

end;

end;

end;

hence 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 ) ; :: thesis: verum

end;

end;

end;

hence 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 ) ; :: thesis: verum

end;

A528: S₁[ 0 ]

proof

let f be FinSequence of (TOP-REAL 2); :: thesis: ( len f = 0 & ( 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
A529: len f = 0 and
A530: 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
f is special and
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 )
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 )
f = {} by A529;
then for n being Nat st n in dom g & n + 1 in dom g holds
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 ;
hence ( g is_sequence_on G & L~ f = L~ g & g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g ) by A530; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A528, A1);
hence ( ( 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 ) ) ; :: thesis: verum