let f be FinSequence of (); :: 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 () 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 () 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 S1[ Nat] means for f being FinSequence of () 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 () 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 S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A2: S1[k] ; :: thesis: S1[k + 1]
let f be FinSequence of (); :: 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 () 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 () 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 () 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 () 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 ;
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 ;
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 ; :: 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 () 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 ;
A16: k <= k + 1 by NAT_1:11;
then A17: k in dom f by ;
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 () ;
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 ;
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 ;
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 ;
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 ; :: 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 ;
then n in dom (f | k) by ;
then A31: (f | k) /. n = f /. n by ;
1 <= n + 1 by NAT_1:11;
then n + 1 in dom (f | k) by ;
then A32: (f | k) /. (n + 1) = f /. (n + 1) by ;
n + 1 <= len f by ;
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 ;
( n in dom f & n + 1 in dom f ) by ;
hence (f | k) /. n <> (f | k) /. (n + 1) by ; :: thesis: verum
end;
then consider g1 being FinSequence of () 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 ;
len c1 = len G by MATRIX_0:def 8;
then A43: dom c1 = dom G by FINSEQ_3:29;
1 <= len f by ;
then A44: k + 1 in dom f by ;
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 ()):] by MATRIX_0:def 4;
then A48: j1 in dom G by ;
A49: i1 in dom G by ;
then A50: X_axis l1 is constant by GOBOARD1:def 4;
A51: i2 in Seg () by ;
then A52: X_axis c1 is increasing by GOBOARD1:def 7;
A53: Y_axis c1 is constant by ;
A54: Y_axis l1 is increasing by ;
A55: len l1 = width G by MATRIX_0:def 7;
A56: j2 in Seg () by ;
A57: dom g1 = Seg (len g1) by FINSEQ_1:def 3;
now :: thesis: ex g being FinSequence of () 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 () 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 () 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 () 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 () 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 ;
then l1 /. j2 = l1 . j2 by PARTFUN1:def 6;
then A60: l1 /. j2 = G * (i1,j2) by ;
then A61: (Y_axis l1) . j2 = (G * (i1,j2)) `2 by ;
i2 in dom l1 by ;
then l1 /. i2 = l1 . i2 by PARTFUN1:def 6;
then A62: l1 /. i2 = G * (i1,i2) by ;
then A63: (Y_axis l1) . i2 = (G * (i1,i2)) `2 by ;
then A64: (G * (i1,j2)) `2 < (G * (i1,i2)) `2 by ;
A65: (X_axis l1) . j2 = (G * (i1,j2)) `1 by ;
(X_axis l1) . i2 = (G * (i1,i2)) `1 by ;
then A66: (G * (i1,i2)) `1 = (G * (i1,j2)) `1 by ;
reconsider l = i2 - j2 as Element of NAT by ;
defpred S2[ Nat, set ] means for m being Nat st m = i2 - \$1 holds
\$2 = G * (i1,m);
set lk = { w where w is Point of () : ( 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 () )
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 () ) )
assume n in Seg l ; :: thesis: ( i2 - n is Element of NAT & [i1,(i2 - n)] in Indices G & i2 - n in Seg () )
then A69: n <= l by FINSEQ_1:1;
l <= i2 by XREAL_1:43;
then reconsider w = i2 - n as Element of NAT by ;
( i2 - n <= i2 & i2 <= width G ) by ;
then A70: w <= width G by XXREAL_0:2;
A71: 1 <= j2 by ;
i2 - l <= i2 - n by ;
then 1 <= w by ;
then w in Seg () by ;
hence ( i2 - n is Element of NAT & [i1,(i2 - n)] in Indices G & i2 - n in Seg () ) by ; :: thesis: verum
end;
A72: now :: thesis: for n being Nat st n in Seg l holds
ex p being Element of the carrier of () st S2[n,p]
let n be Nat; :: thesis: ( n in Seg l implies ex p being Element of the carrier of () st S2[n,p] )
assume n in Seg l ; :: thesis: ex p being Element of the carrier of () st S2[n,p]
then reconsider m = i2 - n as Element of NAT by A68;
take p = G * (i1,m); :: thesis: S2[n,p]
thus S2[n,p] ; :: thesis: verum
end;
consider g2 being FinSequence of () such that
A73: ( len g2 = l & ( for n being Nat st n in Seg l holds
S2[n,g2 /. n] ) ) from 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 ;
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 ;
( [i1,(i2 - n)] in Indices G & g2 /. n = G * (i1,m1) ) by A68, A73, A74, A76;
then ( l1 = i1 & l2 = m1 ) by ;
hence |.(l1 - l3).| + |.(l2 - l4).| = 0 + |.((i2 - n) - (i2 - (n + 1))).| by
.= 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 ;
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 ;
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 ;
( [i1,(i2 - 1)] in Indices G & g2 /. 1 = G * (i1,m1) ) by A68, A73, A74, A89;
then A90: ( l3 = i1 & l4 = m1 ) by ;
(f | k) /. (len (f | k)) = f /. k by ;
then ( l1 = i1 & l2 = i2 ) by ;
hence |.(l1 - l3).| + |.(l2 - l4).| = 0 + |.(i2 - (i2 - 1)).| by
.= 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 ;
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
.= { w where w is Point of () : ( w `1 = (G * (i1,i2)) `1 & (G * (i1,j2)) `2 <= w `2 & w `2 <= (G * (i1,i2)) `2 ) } by ;
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 () 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 () 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 () 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 ;
let p be Point of (); :: 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 ;
then len g1 in dom g1 by FINSEQ_3:25;
then A100: g /. (len g1) = (f | k) /. (len (f | k)) by
.= G * (i1,i2) by ;
hence p `1 = (G * (i1,i2)) `1 by ; :: 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 ; :: thesis: p in rng l1
thus p in rng l1 by ; :: 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 ;
A104: j - (len g1) <> 0 by A101;
then A105: w >= 1 by NAT_1:14;
then A106: w in dom g2 by ;
then reconsider u = i2 - w as Element of NAT by ;
A107: g /. j = g2 /. w by ;
A108: (X_axis l1) . i2 = (G * (i1,i2)) `1 by ;
A109: u < i2 by ;
A110: g2 /. w = G * (i1,u) by ;
A111: i2 - w in Seg () by ;
then u in dom l1 by ;
then l1 /. u = l1 . u by PARTFUN1:def 6;
then A112: l1 /. u = G * (i1,u) by ;
then A113: (Y_axis l1) . u = (G * (i1,u)) `2 by ;
(X_axis l1) . u = (G * (i1,u)) `1 by ;
hence p `1 = (G * (i1,i2)) `1 by ; :: 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 ;
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 ; :: thesis: verum
end;
suppose A115: u <> j2 ; :: thesis: (G * (i1,j2)) `2 <= p `2
i2 - (len g2) <= u by ;
then j2 < u by ;
hence (G * (i1,j2)) `2 <= p `2 by ; :: 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 ;
hence p `2 <= (G * (i1,i2)) `2 by ; :: thesis: p in rng l1
thus p in rng l1 by ; :: 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 ;
then A122: i in dom g1 by ;
1 <= i + 1 by NAT_1:11;
then i + 1 in dom g1 by ;
then X = LSeg (g1,i) by ;
then X in { (LSeg (g1,j)) where j is Nat : ( 1 <= j & j + 1 <= len g1 ) } by ;
then A123: x in L~ (f | k) by ;
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 () ;
A125: i <= len g by ;
A126: len g1 <= i by ;
then A127: q1 `1 = (G * (i1,i2)) `1 by ;
A128: q1 `2 <= (G * (i1,i2)) `2 by ;
A129: (G * (i1,j2)) `2 <= q1 `2 by ;
q2 `1 = (G * (i1,i2)) `1 by ;
then A130: q2 = |[(q1 `1),(q2 `2)]| by ;
A131: q2 `2 <= (G * (i1,i2)) `2 by ;
A132: ( q1 = |[(q1 `1),(q1 `2)]| & LSeg (g,i) = LSeg (q2,q1) ) by ;
A133: (G * (i1,j2)) `2 <= q2 `2 by ;
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 () : ( p2 `1 = q1 `1 & q2 `2 <= p2 `2 & p2 `2 <= q1 `2 ) } by ;
then consider p2 being Point of () such that
A134: ( p2 = x & p2 `1 = q1 `1 ) and
A135: ( q2 `2 <= p2 `2 & p2 `2 <= q1 `2 ) by ;
( (G * (i1,j2)) `2 <= p2 `2 & p2 `2 <= (G * (i1,i2)) `2 ) by ;
then A136: x in LSeg (f,k) by ;
LSeg (f,k) in { (LSeg (f,j)) where j is Nat : ( 1 <= j & j + 1 <= len f ) } by ;
hence x in L~ f by ; :: thesis: verum
end;
suppose q1 `2 = q2 `2 ; :: thesis: x in L~ f
then LSeg (g,i) = {q1} by ;
then x = q1 by ;
then A137: x in LSeg (f,k) by ;
LSeg (f,k) in { (LSeg (f,j)) where j is Nat : ( 1 <= j & j + 1 <= len f ) } by ;
hence x in L~ f by ; :: thesis: verum
end;
suppose q1 `2 < q2 `2 ; :: thesis: x in L~ f
then LSeg (g,i) = { p1 where p1 is Point of () : ( p1 `1 = q1 `1 & q1 `2 <= p1 `2 & p1 `2 <= q2 `2 ) } by ;
then consider p2 being Point of () such that
A138: ( p2 = x & p2 `1 = q1 `1 ) and
A139: ( q1 `2 <= p2 `2 & p2 `2 <= q2 `2 ) by ;
( (G * (i1,j2)) `2 <= p2 `2 & p2 `2 <= (G * (i1,i2)) `2 ) by ;
then A140: x in LSeg (f,k) by ;
LSeg (f,k) in { (LSeg (f,j)) where j is Nat : ( 1 <= j & j + 1 <= len f ) } by ;
hence x in L~ f by ; :: 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 ;
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 ; :: thesis: verum
end;
suppose x in LSeg (f,k) ; :: thesis: x in L~ g
then consider p1 being Point of () 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 S3[ Nat] means ( len g1 <= \$1 & \$1 <= len g & ( for q being Point of () st q = g /. \$1 holds
q `2 >= p1 `2 ) );
A147: now :: thesis: ex n being Nat st S3[n]
reconsider n = len g1 as Nat ;
take n = n; :: thesis: S3[n]
thus S3[n] :: thesis: verum
proof
thus ( len g1 <= n & n <= len g ) by ; :: thesis: for q being Point of () st q = g /. n holds
q `2 >= p1 `2

1 <= len g1 by ;
then A148: len g1 in dom g1 by FINSEQ_3:25;
let q be Point of (); :: 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
.= G * (i1,i2) by ;
hence q `2 >= p1 `2 by A146; :: thesis: verum
end;
end;
A149: for n being Nat st S3[n] holds
n <= len g ;
consider ma being Nat such that
A150: ( S3[ma] & ( for n being Nat st S3[n] holds
n <= ma ) ) from 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 ;
then A152: 1 <= l by XREAL_1:19;
then 0 + 1 <= ma by ;
then reconsider m1 = ma - 1 as Element of NAT by INT_1:5;
A153: m1 + 1 = ma ;
(len g1) + 1 <= ma by ;
then A154: m1 >= len g1 by ;
reconsider q = g /. m1 as Point of () ;
set lq = { e where e is Point of () : ( 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 ;
then A157: g /. ma = g2 /. l by
.= G * (i1,j2) by ;
then p1 `2 <= (G * (i1,j2)) `2 by A150;
then A158: p1 `2 = (G * (i1,j2)) `2 by ;
A159: m1 <= len g by ;
then A160: q `1 = (G * (i1,i2)) `1 by ;
A161: (G * (i1,j2)) `2 <= q `2 by ;
1 <= len g1 by ;
then A162: 1 <= m1 by ;
then ( q = |[(q `1),(q `2)]| & LSeg (g,m1) = LSeg ((G * (i1,j2)),q) ) by ;
then LSeg (g,m1) = { e where e is Point of () : ( e `1 = (G * (i1,i2)) `1 & (G * (i1,j2)) `2 <= e `2 & e `2 <= q `2 ) } by ;
then A163: p1 in LSeg (g,m1) by ;
LSeg (g,m1) in { (LSeg (g,i)) where i is Nat : ( 1 <= i & i + 1 <= len g ) } by ;
hence x in L~ g by ; :: thesis: verum
end;
suppose ma <> len g ; :: thesis: x in L~ g
then ma < len g by ;
then A164: ma + 1 <= len g by NAT_1:13;
reconsider qa = g /. ma, qa1 = g /. (ma + 1) as Point of () ;
set lma = { p2 where p2 is Point of () : ( 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 ;
then A168: qa1 `1 = (G * (i1,i2)) `1 by ;
A169: now :: thesis: not p1 `2 <= qa1 `2
assume p1 `2 <= qa1 `2 ; :: thesis: contradiction
then for q being Point of () st q = g /. (ma + 1) holds
p1 `2 <= q `2 ;
then ma + 1 <= ma by ;
hence contradiction by XREAL_1:29; :: thesis: verum
end;
A170: ( qa `1 = (G * (i1,i2)) `1 & qa = |[(qa `1),(qa `2)]| ) by ;
A171: 1 <= ma by ;
then LSeg (g,ma) = LSeg (qa1,qa) by
.= { p2 where p2 is Point of () : ( p2 `1 = (G * (i1,i2)) `1 & qa1 `2 <= p2 `2 & p2 `2 <= qa `2 ) } by ;
then A172: x in LSeg (g,ma) by ;
LSeg (g,ma) in { (LSeg (g,i)) where i is Nat : ( 1 <= i & i + 1 <= len g ) } by ;
hence x in L~ g by ; :: 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 ;
then 1 in dom g1 by FINSEQ_3:25;
hence g /. 1 = (f | k) /. 1 by
.= f /. 1 by ;
:: 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 ;
then A174: 1 <= l by XREAL_1:19;
then A175: l in dom g2 by ;
hence g /. (len g) = g2 /. l by
.= G * (i1,m1) by
.= f /. (len f) by A3, A46, A58 ;
:: thesis: len f <= len g
thus len f <= len g by ; :: thesis: verum
end;
case A176: i2 < j2 ; :: thesis: ex g being FinSequence of the carrier of () 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 () : ( 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 ;
deffunc H1( Nat) -> Element of the carrier of () = G * (i1,(i2 + \$1));
consider g2 being FinSequence of () such that
A178: ( len g2 = l & ( for n being Nat st n in dom g2 holds
g2 /. n = H1(n) ) ) from 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 () & [i1,(i2 + n)] in Indices G )
let n be Nat; :: thesis: ( n in Seg l implies ( i2 + n in Seg () & [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 () & [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 ;
then A183: i2 + n <= width G by ;
1 <= n by ;
then 1 <= i2 + n by ;
hence i2 + n in Seg () by ; :: thesis: [i1,(i2 + n)] in Indices G
hence [i1,(i2 + n)] in Indices G by ; :: 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 ; :: 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 ;
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 ;
then A194: ( l3 = i1 & l4 = i2 + (n + 1) ) by ;
( g2 /. n = G * (i1,(i2 + n)) & [i1,(i2 + n)] in Indices G ) by ;
then ( l1 = i1 & l2 = i2 + n ) by ;
hence |.(l1 - l3).| + |.(l2 - l4).| = 0 + |.((i2 + n) - (i2 + (n + 1))).| by
.= |.(- 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 ;
then A200: ( l3 = i1 & l4 = i2 + 1 ) by ;
(f | k) /. (len (f | k)) = f /. k by ;
then ( l1 = i1 & l2 = i2 ) by ;
hence |.(l1 - l3).| + |.(l2 - l4).| = 0 + |.(i2 - (i2 + 1)).| by
.= |.((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 ;
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 ;
then l1 /. j2 = l1 . j2 by PARTFUN1:def 6;
then A202: l1 /. j2 = G * (i1,j2) by ;
then A203: (Y_axis l1) . j2 = (G * (i1,j2)) `2 by ;
i2 in dom l1 by ;
then l1 /. i2 = l1 . i2 by PARTFUN1:def 6;
then A204: l1 /. i2 = G * (i1,i2) by ;
then A205: (Y_axis l1) . i2 = (G * (i1,i2)) `2 by ;
then A206: (G * (i1,i2)) `2 < (G * (i1,j2)) `2 by ;
A207: (X_axis l1) . j2 = (G * (i1,j2)) `1 by ;
(X_axis l1) . i2 = (G * (i1,i2)) `1 by ;
then A208: (G * (i1,i2)) `1 = (G * (i1,j2)) `1 by ;
A209: LSeg (f,k) = LSeg ((G * (i1,i2)),(G * (i1,j2))) by
.= { w where w is Point of () : ( w `1 = (G * (i1,i2)) `1 & (G * (i1,i2)) `2 <= w `2 & w `2 <= (G * (i1,j2)) `2 ) } by ;
A210: dom g2 = Seg l by ;
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 () 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 () 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 () 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 ;
let p be Point of (); :: 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 ;
then len g1 in dom g1 by FINSEQ_3:25;
then A218: g /. (len g1) = (f | k) /. (len (f | k)) by
.= G * (i1,i2) by ;
hence p `1 = (G * (i1,i2)) `1 by ; :: 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 ; :: thesis: p in rng l1
thus p in rng l1 by ; :: 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 ;
A222: (X_axis l1) . i2 = (G * (i1,i2)) `1 by ;
A223: j - (len g1) <> 0 by A219;
then A224: w >= 1 by NAT_1:14;
then A225: g /. j = g2 /. w by ;
A226: i2 < i2 + w by ;
A227: w in dom g2 by ;
then A228: i2 + w in Seg () by ;
i2 + w in Seg () by ;
then i2 + w in dom l1 by ;
then l1 /. (i2 + w) = l1 . (i2 + w) by PARTFUN1:def 6;
then A229: l1 /. (i2 + w) = G * (i1,(i2 + w)) by ;
then A230: (Y_axis l1) . (i2 + w) = (G * (i1,(i2 + w))) `2 by ;
A231: g2 /. w = G * (i1,(i2 + w)) by ;
(X_axis l1) . (i2 + w) = (G * (i1,(i2 + w))) `1 by ;
hence p `1 = (G * (i1,i2)) `1 by ; :: 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 ;
hence (G * (i1,i2)) `2 <= p `2 by ; :: thesis: ( p `2 <= (G * (i1,j2)) `2 & p in rng l1 )
A232: (Y_axis l1) . j2 = (G * (i1,j2)) `2 by ;
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 ; :: thesis: verum
end;
suppose A233: i2 + w <> j2 ; :: thesis: p `2 <= (G * (i1,j2)) `2
i2 + w <= i2 + l by ;
then i2 + w < j2 by ;
hence p `2 <= (G * (i1,j2)) `2 by ; :: thesis: verum
end;
end;
end;
hence p `2 <= (G * (i1,j2)) `2 ; :: thesis: p in rng l1
thus p in rng l1 by ; :: 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 ;
then A240: i in dom g1 by ;
1 <= i + 1 by NAT_1:11;
then i + 1 in dom g1 by ;
then X = LSeg (g1,i) by ;
then X in { (LSeg (g1,j)) where j is Nat : ( 1 <= j & j + 1 <= len g1 ) } by ;
then A241: x in L~ (f | k) by ;
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 () ;
A243: i <= len g by ;
A244: len g1 <= i by ;
then A245: q1 `1 = (G * (i1,i2)) `1 by ;
A246: q1 `2 <= (G * (i1,j2)) `2 by ;
A247: (G * (i1,i2)) `2 <= q1 `2 by ;
q2 `1 = (G * (i1,i2)) `1 by ;
then A248: q2 = |[(q1 `1),(q2 `2)]| by ;
A249: q2 `2 <= (G * (i1,j2)) `2 by ;
A250: ( q1 = |[(q1 `1),(q1 `2)]| & LSeg (g,i) = LSeg (q2,q1) ) by ;
A251: (G * (i1,i2)) `2 <= q2 `2 by ;
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 () : ( p2 `1 = q1 `1 & q2 `2 <= p2 `2 & p2 `2 <= q1 `2 ) } by ;
then consider p2 being Point of () such that
A252: ( p2 = x & p2 `1 = q1 `1 ) and
A253: ( q2 `2 <= p2 `2 & p2 `2 <= q1 `2 ) by ;
( (G * (i1,i2)) `2 <= p2 `2 & p2 `2 <= (G * (i1,j2)) `2 ) by ;
then A254: x in LSeg (f,k) by ;
LSeg (f,k) in { (LSeg (f,j)) where j is Nat : ( 1 <= j & j + 1 <= len f ) } by ;
hence x in L~ f by ; :: thesis: verum
end;
suppose q1 `2 = q2 `2 ; :: thesis: x in L~ f
then LSeg (g,i) = {q1} by ;
then x = q1 by ;
then A255: x in LSeg (f,k) by ;
LSeg (f,k) in { (LSeg (f,j)) where j is Nat : ( 1 <= j & j + 1 <= len f ) } by ;
hence x in L~ f by ; :: thesis: verum
end;
suppose q1 `2 < q2 `2 ; :: thesis: x in L~ f
then LSeg (g,i) = { p1 where p1 is Point of () : ( p1 `1 = q1 `1 & q1 `2 <= p1 `2 & p1 `2 <= q2 `2 ) } by ;
then consider p2 being Point of () such that
A256: ( p2 = x & p2 `1 = q1 `1 ) and
A257: ( q1 `2 <= p2 `2 & p2 `2 <= q2 `2 ) by ;
( (G * (i1,i2)) `2 <= p2 `2 & p2 `2 <= (G * (i1,j2)) `2 ) by ;
then A258: x in LSeg (f,k) by ;
LSeg (f,k) in { (LSeg (f,j)) where j is Nat : ( 1 <= j & j + 1 <= len f ) } by ;
hence x in L~ f by ; :: 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 ;
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 ; :: thesis: verum
end;
suppose x in LSeg (f,k) ; :: thesis: x in L~ g
then consider p1 being Point of () 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 S2[ Nat] means ( len g1 <= \$1 & \$1 <= len g & ( for q being Point of () st q = g /. \$1 holds
q `2 <= p1 `2 ) );
A265: now :: thesis: ex n being Nat st S2[n]
reconsider n = len g1 as Nat ;
take n = n; :: thesis: S2[n]
thus S2[n] :: thesis: verum
proof
thus ( len g1 <= n & n <= len g ) by ; :: thesis: for q being Point of () st q = g /. n holds
q `2 <= p1 `2

1 <= len g1 by ;
then A266: len g1 in dom g1 by FINSEQ_3:25;
let q be Point of (); :: 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
.= G * (i1,i2) by ;
hence q `2 <= p1 `2 by A263; :: thesis: verum
end;
end;
A267: for n being Nat st S2[n] holds
n <= len g ;
consider ma being Nat such that
A268: ( S2[ma] & ( for n being Nat st S2[n] holds
n <= ma ) ) from 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 ;
then A270: 1 <= l by XREAL_1:19;
then 0 + 1 <= ma by ;
then reconsider m1 = ma - 1 as Element of NAT by INT_1:5;
A271: m1 + 1 = ma ;
(len g1) + 1 <= ma by ;
then A272: m1 >= len g1 by ;
reconsider q = g /. m1 as Point of () ;
set lq = { e where e is Point of () : ( 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 ;
then A275: g /. ma = g2 /. l by
.= G * (i1,j2) by ;
then (G * (i1,j2)) `2 <= p1 `2 by A268;
then A276: p1 `2 = (G * (i1,j2)) `2 by ;
A277: m1 <= len g by ;
then A278: q `1 = (G * (i1,i2)) `1 by ;
A279: q `2 <= (G * (i1,j2)) `2 by ;
1 <= len g1 by ;
then A280: 1 <= m1 by ;
then ( q = |[(q `1),(q `2)]| & LSeg (g,m1) = LSeg ((G * (i1,j2)),q) ) by ;
then LSeg (g,m1) = { e where e is Point of () : ( e `1 = (G * (i1,i2)) `1 & q `2 <= e `2 & e `2 <= (G * (i1,j2)) `2 ) } by ;
then A281: p1 in LSeg (g,m1) by ;
LSeg (g,m1) in { (LSeg (g,i)) where i is Nat : ( 1 <= i & i + 1 <= len g ) } by ;
hence x in L~ g by ; :: thesis: verum
end;
suppose ma <> len g ; :: thesis: x in L~ g
then ma < len g by ;
then A282: ma + 1 <= len g by NAT_1:13;
reconsider qa = g /. ma, qa1 = g /. (ma + 1) as Point of () ;
set lma = { p2 where p2 is Point of () : ( 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 ;
then A286: qa1 `1 = (G * (i1,i2)) `1 by ;
A287: now :: thesis: not qa1 `2 <= p1 `2
assume qa1 `2 <= p1 `2 ; :: thesis: contradiction
then for q being Point of () st q = g /. (ma + 1) holds
q `2 <= p1 `2 ;
then ma + 1 <= ma by ;
hence contradiction by XREAL_1:29; :: thesis: verum
end;
A288: ( qa `1 = (G * (i1,i2)) `1 & qa = |[(qa `1),(qa `2)]| ) by ;
A289: 1 <= ma by ;
then LSeg (g,ma) = LSeg (qa,qa1) by
.= { p2 where p2 is Point of () : ( p2 `1 = (G * (i1,i2)) `1 & qa `2 <= p2 `2 & p2 `2 <= qa1 `2 ) } by ;
then A290: x in LSeg (g,ma) by ;
LSeg (g,ma) in { (LSeg (g,i)) where i is Nat : ( 1 <= i & i + 1 <= len g ) } by ;
hence x in L~ g by ; :: 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 ;
then 1 in dom g1 by FINSEQ_3:25;
hence g /. 1 = (f | k) /. 1 by
.= f /. 1 by ;
:: thesis: ( g /. (len g) = f /. (len f) & len f <= len g )
A291: len g = (len g1) + l by ;
i2 + 1 <= j2 by ;
then A292: 1 <= l by XREAL_1:19;
then A293: l in dom g2 by ;
hence g /. (len g) = g2 /. l by
.= G * (i1,(i2 + l)) by
.= f /. (len f) by A3, A46, A58 ;
:: thesis: len f <= len g
thus len f <= len g by ; :: thesis: verum
end;
end;
end;
hence ex g being FinSequence of () 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 () 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 () 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 () 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 () 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 ;
then A296: c1 /. j1 = G * (j1,i2) by ;
then A297: (X_axis c1) . j1 = (G * (j1,i2)) `1 by ;
c1 /. i1 = c1 . i1 by ;
then A298: c1 /. i1 = G * (i1,i2) by ;
then A299: (X_axis c1) . i1 = (G * (i1,i2)) `1 by ;
then A300: (G * (j1,i2)) `1 < (G * (i1,i2)) `1 by ;
A301: (Y_axis c1) . j1 = (G * (j1,i2)) `2 by ;
(Y_axis c1) . i1 = (G * (i1,i2)) `2 by ;
then A302: (G * (i1,i2)) `2 = (G * (j1,i2)) `2 by ;
reconsider l = i1 - j1 as Element of NAT by ;
defpred S2[ Nat, set ] means for m being Nat st m = i1 - \$1 holds
\$2 = G * (m,i2);
set lk = { w where w is Point of () : ( 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 ;
( i1 - n <= i1 & i1 <= len G ) by ;
then A306: w <= len G by XXREAL_0:2;
A307: 1 <= j1 by ;
i1 - l <= i1 - n by ;
then 1 <= w by ;
then w in dom G by ;
hence ( i1 - n is Element of NAT & [(i1 - n),i2] in Indices G & i1 - n in dom G ) by ; :: thesis: verum
end;
A308: now :: thesis: for n being Nat st n in Seg l holds
ex p being Element of the carrier of () st S2[n,p]
let n be Nat; :: thesis: ( n in Seg l implies ex p being Element of the carrier of () st S2[n,p] )
assume n in Seg l ; :: thesis: ex p being Element of the carrier of () st S2[n,p]
then reconsider m = i1 - n as Element of NAT by A304;
take p = G * (m,i2); :: thesis: S2[n,p]
thus S2[n,p] ; :: thesis: verum
end;
consider g2 being FinSequence of () such that
A309: ( len g2 = l & ( for n being Nat st n in Seg l holds
S2[n,g2 /. n] ) ) from 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 ;
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 ;
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 ;
then A318: ( l3 = m2 & l4 = i2 ) by ;
( [(i1 - n),i2] in Indices G & g2 /. n = G * (m1,i2) ) by ;
then ( l1 = m1 & l2 = i2 ) by ;
hence |.(l1 - l3).| + |.(l2 - l4).| = |.((i1 - n) - (i1 - (n + 1))).| + 0 by
.= 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 ;
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 ; :: 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 ;
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 ;
( [(i1 - 1),i2] in Indices G & g2 /. 1 = G * (m1,i2) ) by ;
then A326: ( l3 = m1 & l4 = i2 ) by ;
(f | k) /. (len (f | k)) = f /. k by ;
then ( l1 = i1 & l2 = i2 ) by ;
hence |.(l1 - l3).| + |.(l2 - l4).| = |.(i1 - (i1 - 1)).| + 0 by
.= 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 ;
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
.= { w where w is Point of () : ( w `2 = (G * (i1,i2)) `2 & (G * (j1,i2)) `1 <= w `1 & w `1 <= (G * (i1,i2)) `1 ) } by ;
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 () 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 () 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 () 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 ;
let p be Point of (); :: 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 ;
then len g1 in dom g1 by FINSEQ_3:25;
then A335: g /. (len g1) = (f | k) /. (len (f | k)) by
.= G * (i1,i2) by ;
hence p `2 = (G * (i1,i2)) `2 by ; :: 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 ; :: thesis: p in rng c1
thus p in rng c1 by ; :: 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 ;
A339: j - (len g1) <> 0 by A336;
then A340: w >= 1 by NAT_1:14;
then A341: w in dom g2 by ;
then reconsider u = i1 - w as Element of NAT by ;
A342: g /. j = g2 /. w by ;
A343: u < i1 by ;
A344: g2 /. w = G * (u,i2) by ;
A345: (Y_axis c1) . i1 = (G * (i1,i2)) `2 by ;
A346: i1 - w in dom G by ;
c1 /. u = c1 . u by ;
then A347: c1 /. u = G * (u,i2) by ;
then A348: (X_axis c1) . u = (G * (u,i2)) `1 by ;
(Y_axis c1) . u = (G * (u,i2)) `2 by ;
hence p `2 = (G * (i1,i2)) `2 by ; :: 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 ;
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 ; :: thesis: verum
end;
suppose A350: u <> j1 ; :: thesis: (G * (j1,i2)) `1 <= p `1
i1 - (len g2) <= u by ;
then j1 < u by ;
hence (G * (j1,i2)) `1 <= p `1 by ; :: 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 ;
hence p `1 <= (G * (i1,i2)) `1 by ; :: thesis: p in rng c1
thus p in rng c1 by ; :: 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 ;
then A357: i in dom g1 by ;
1 <= i + 1 by NAT_1:11;
then i + 1 in dom g1 by ;
then X = LSeg (g1,i) by ;
then X in { (LSeg (g1,j)) where j is Nat : ( 1 <= j & j + 1 <= len g1 ) } by ;
then A358: x in L~ (f | k) by ;
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 () ;
A360: i <= len g by ;
A361: len g1 <= i by ;
then A362: q1 `2 = (G * (i1,i2)) `2 by ;
A363: q1 `1 <= (G * (i1,i2)) `1 by ;
A364: (G * (j1,i2)) `1 <= q1 `1 by ;
q2 `2 = (G * (i1,i2)) `2 by ;
then A365: q2 = |[(q2 `1),(q1 `2)]| by ;
A366: q2 `1 <= (G * (i1,i2)) `1 by ;
A367: ( q1 = |[(q1 `1),(q1 `2)]| & LSeg (g,i) = LSeg (q2,q1) ) by ;
A368: (G * (j1,i2)) `1 <= q2 `1 by ;
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 () : ( p2 `2 = q1 `2 & q2 `1 <= p2 `1 & p2 `1 <= q1 `1 ) } by ;
then consider p2 being Point of () such that
A369: ( p2 = x & p2 `2 = q1 `2 ) and
A370: ( q2 `1 <= p2 `1 & p2 `1 <= q1 `1 ) by ;
( (G * (j1,i2)) `1 <= p2 `1 & p2 `1 <= (G * (i1,i2)) `1 ) by ;
then A371: x in LSeg (f,k) by ;
LSeg (f,k) in { (LSeg (f,j)) where j is Nat : ( 1 <= j & j + 1 <= len f ) } by ;
hence x in L~ f by ; :: thesis: verum
end;
suppose q1 `1 = q2 `1 ; :: thesis: x in L~ f
then LSeg (g,i) = {q1} by ;
then x = q1 by ;
then A372: x in LSeg (f,k) by ;
LSeg (f,k) in { (LSeg (f,j)) where j is Nat : ( 1 <= j & j + 1 <= len f ) } by ;
hence x in L~ f by ; :: thesis: verum
end;
suppose q1 `1 < q2 `1 ; :: thesis: x in L~ f
then LSeg (g,i) = { p1 where p1 is Point of () : ( p1 `2 = q1 `2 & q1 `1 <= p1 `1 & p1 `1 <= q2 `1 ) } by ;
then consider p2 being Point of () such that
A373: ( p2 = x & p2 `2 = q1 `2 ) and
A374: ( q1 `1 <= p2 `1 & p2 `1 <= q2 `1 ) by ;
( (G * (j1,i2)) `1 <= p2 `1 & p2 `1 <= (G * (i1,i2)) `1 ) by ;
then A375: x in LSeg (f,k) by ;
LSeg (f,k) in { (LSeg (f,j)) where j is Nat : ( 1 <= j & j + 1 <= len f ) } by ;
hence x in L~ f by ; :: 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 ;
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 ; :: thesis: verum
end;
suppose x in LSeg (f,k) ; :: thesis: x in L~ g
then consider p1 being Point of () 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 S3[ Nat] means ( len g1 <= \$1 & \$1 <= len g & ( for q being Point of () st q = g /. \$1 holds
q `1 >= p1 `1 ) );
A382: now :: thesis: ex n being Nat st S3[n]
reconsider n = len g1 as Nat ;
take n = n; :: thesis: S3[n]
thus S3[n] :: thesis: verum
proof
thus ( len g1 <= n & n <= len g ) by ; :: thesis: for q being Point of () st q = g /. n holds
q `1 >= p1 `1

1 <= len g1 by ;
then A383: len g1 in dom g1 by FINSEQ_3:25;
let q be Point of (); :: 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
.= G * (i1,i2) by ;
hence q `1 >= p1 `1 by A381; :: thesis: verum
end;
end;
A384: for n being Nat st S3[n] holds
n <= len g ;
consider ma being Nat such that
A385: ( S3[ma] & ( for n being Nat st S3[n] holds
n <= ma ) ) from 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 ;
then A387: 1 <= l by XREAL_1:19;
then 0 + 1 <= ma by ;
then reconsider m1 = ma - 1 as Element of NAT by INT_1:5;
A388: m1 + 1 = ma ;
(len g1) + 1 <= ma by ;
then A389: m1 >= len g1 by ;
reconsider q = g /. m1 as Point of () ;
set lq = { e where e is Point of () : ( 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 ;
then A392: g /. ma = g2 /. l by
.= G * (j1,i2) by ;
then p1 `1 <= (G * (j1,i2)) `1 by A385;
then A393: p1 `1 = (G * (j1,i2)) `1 by ;
A394: m1 <= len g by ;
then A395: q `2 = (G * (i1,i2)) `2 by ;
A396: (G * (j1,i2)) `1 <= q `1 by ;
1 <= len g1 by ;
then A397: 1 <= m1 by ;
then ( q = |[(q `1),(q `2)]| & LSeg (g,m1) = LSeg ((G * (j1,i2)),q) ) by ;
then LSeg (g,m1) = { e where e is Point of () : ( e `2 = (G * (i1,i2)) `2 & (G * (j1,i2)) `1 <= e `1 & e `1 <= q `1 ) } by ;
then A398: p1 in LSeg (g,m1) by ;
LSeg (g,m1) in { (LSeg (g,i)) where i is Nat : ( 1 <= i & i + 1 <= len g ) } by ;
hence x in L~