let f be FinSequence of (TOP-REAL 2); :: thesis:
let G be Go-board; :: thesis:
defpred S₂[ Element of NAT ] means for f being FinSequence of (TOP-REAL 2) st len f = $1 & ( for n being Element of NAT st n in dom f holds
ex i, j being Element of NAT st
( [i,j] in Indices G & f /. n = G * i,j ) ) & f is special & ( for n being Element of 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: S₂[ 0 ]

proof

let f be FinSequence of (TOP-REAL 2); :: thesis:
assume A2: ( len f = 0 & ( for n being Element of NAT st n in dom f holds
ex i, j being Element of NAT st
( [i,j] in Indices G & f /. n = G * i,j ) ) & f is special & ( for n being Element of NAT st n in dom f & n + 1 in dom f holds
f /. n <> f /. (n + 1) ) ) ; :: thesis:
take g = f; :: thesis:
f = {} by A2;
then for n being Element of NAT st n in dom g & n + 1 in dom g holds
for m, k, i, j being Element of NAT st [m,k] in Indices G & [i,j] in Indices G & g /. n = G * m,k & g /. (n + 1) = G * i,j holds
(abs (m - i)) + (abs (k - j)) = 1 by RELAT_1:60;
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 A2, GOBOARD1:def 11; :: thesis:

end;

A3: for k being Element of NAT st S₂[k] holds
S₂[k + 1]

proof

let k be Element of NAT ; :: thesis:
assume A4: S₂[k] ; :: thesis:
let f be FinSequence of (TOP-REAL 2); :: thesis:
assume that
A5: len f = k + 1 and
A6: for n being Element of NAT st n in dom f holds
ex i, j being Element of NAT st
( [i,j] in Indices G & f /. n = G * i,j ) and
A7: f is special and
A8: for n being Element of NAT st n in dom f & n + 1 in dom f holds
f /. n <> f /. (n + 1) ; :: thesis:
A9: dom f = Seg (len f) by FINSEQ_1:def 3;

now

per cases ;

suppose k = 0 ; :: thesis:

then A10: dom f = {1} by A5, FINSEQ_1:4, FINSEQ_1:def 3;
take g = f; :: thesis:

now

let n be Element of NAT ; :: thesis:
assume ( n in dom g & n + 1 in dom g ) ; :: thesis:
then ( n = 1 & n + 1 = 1 ) by A10, TARSKI:def 1;
hence for i1, i2, j1, j2 being Element of NAT st [i1,i2] in Indices G & [j1,j2] in Indices G & g /. n = G * i1,i2 & g /. (n + 1) = G * j1,j2 holds
(abs (i1 - j1)) + (abs (i2 - j2)) = 1 ; :: thesis:

end;

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 A6, GOBOARD1:def 11; :: thesis:

end;

suppose A11: k <> 0 ; :: thesis:

then A12: ( 0 < k & k <= k + 1 ) by NAT_1:11;
then A13: ( 0 + 1 <= k & k <= len f & k + 1 <= len f ) by A5, NAT_1:13;
then A14: ( k in dom f & len (f | k) = k & dom (f | k) = Seg (len (f | k)) & k in Seg k & 1 in Seg k ) by A9, FINSEQ_1:3, FINSEQ_1:80, FINSEQ_1:def 3;
set f1 = f | k;

A15: now

let n be Element of NAT ; :: thesis:
assume A16: n in dom (f | k) ; :: thesis:
then ( (f | k) /. n = f /. n & n in dom f ) by A14, FINSEQ_4:86;
then consider i, j being Element of NAT such that
A17: ( [i,j] in Indices G & f /. n = G * i,j ) by A6;
take i = i; :: thesis:
take j = j; :: thesis:
thus ( [i,j] in Indices G & (f | k) /. n = G * i,j ) by A14, A16, A17, FINSEQ_4:86; :: thesis:

end;

A18: f | k is special

proof

let n be Nat; :: according to TOPREAL1:def 7 :: thesis:
set p = (f | k) /. n;
set q = (f | k) /. (n + 1);
assume A19: ( 1 <= n & n + 1 <= len (f | k) ) ; :: thesis:
n <= n + 1 by NAT_1:11;
then ( 1 <= n + 1 & n <= len (f | k) ) by A19, XXREAL_0:2;
then ( n in dom (f | k) & n + 1 in dom (f | k) ) by A19, FINSEQ_3:27;
then A20: ( (f | k) /. n = f /. n & (f | k) /. (n + 1) = f /. (n + 1) ) by A14, FINSEQ_4:86;
n + 1 <= len f by A5, A12, A14, A19, XXREAL_0:2;
hence ( ((f | k) /. n) `1 = ((f | k) /. (n + 1)) `1 or ((f | k) /. n) `2 = ((f | k) /. (n + 1)) `2 ) by A7, A19, A20, TOPREAL1:def 7; :: thesis:

end;

now

let n be Element of NAT ; :: thesis:
assume A21: ( n in dom (f | k) & n + 1 in dom (f | k) ) ; :: thesis:
then A22: ( n in dom f & n + 1 in dom f ) by A14, FINSEQ_4:86;
( (f | k) /. n = f /. n & (f | k) /. (n + 1) = f /. (n + 1) ) by A14, A21, FINSEQ_4:86;
hence (f | k) /. n <> (f | k) /. (n + 1) by A8, A22; :: thesis:

end;

then consider g1 being FinSequence of (TOP-REAL 2) such that
A23: ( g1 is_sequence_on G & L~ g1 = L~ (f | k) & g1 /. 1 = (f | k) /. 1 & g1 /. (len g1) = (f | k) /. (len (f | k)) & len (f | k) <= len g1 ) by A4, A14, A15, A18;
consider i1, i2 being Element of NAT such that
A24: ( [i1,i2] in Indices G & f /. k = G * i1,i2 ) by A6, A14;
1 <= len f by A13, XXREAL_0:2;
then A25: k + 1 in dom f by A5, FINSEQ_3:27;
then consider j1, j2 being Element of NAT such that
A26: ( [j1,j2] in Indices G & f /. (k + 1) = G * j1,j2 ) by A6;
A27: Indices G = [:(dom G),(Seg (width G)):] by MATRIX_1:def 5;
then A28: ( i1 in dom G & i2 in Seg (width G) & j1 in dom G & j2 in Seg (width G) ) by A24, A26, ZFMISC_1:106;
A29: ( ( for n being Element of NAT st n in dom g1 holds
ex m, k being Element of NAT st
( [m,k] in Indices G & g1 /. n = G * m,k ) ) & ( for n being Element of NAT st n in dom g1 & n + 1 in dom g1 holds
for m, k, i, j being Element of NAT st [m,k] in Indices G & [i,j] in Indices G & g1 /. n = G * m,k & g1 /. (n + 1) = G * i,j holds
(abs (m - i)) + (abs (k - j)) = 1 ) ) by A23, GOBOARD1:def 11;
A30: dom g1 = Seg (len g1) by FINSEQ_1:def 3;
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;
A31: X_axis l1 is constant by A28, GOBOARD1:def 6;
A32: Y_axis l1 is increasing by A28, GOBOARD1:def 8;
A33: X_axis c1 is increasing by A28, GOBOARD1:def 9;
A34: Y_axis c1 is constant by A28, GOBOARD1:def 7;
A35: dom (X_axis l1) = Seg (len (X_axis l1)) by FINSEQ_1:def 3;
A36: dom (Y_axis l1) = Seg (len (Y_axis l1)) by FINSEQ_1:def 3;
A37: len (Y_axis l1) = len l1 by GOBOARD1:def 4;
A38: len (X_axis l1) = len l1 by GOBOARD1:def 3;
A39: len l1 = width G by MATRIX_1:def 8;
A40: len (X_axis c1) = len c1 by GOBOARD1:def 3;
A41: len (Y_axis c1) = len c1 by GOBOARD1:def 4;
len c1 = len G by MATRIX_1:def 9;
then A42: dom c1 = dom G by FINSEQ_3:31;
A43: ( dom (Y_axis l1) = dom l1 & dom (X_axis l1) = dom l1 & dom (X_axis c1) = dom c1 & dom (Y_axis c1) = dom c1 ) by A37, A38, A40, A41, FINSEQ_3:31;

now

per cases by A7, A14, A24, A25, A26, Th16;

suppose A44: i1 = j1 ; :: thesis:

set ppi = G * i1,i2;
set pj = G * i1,j2;

now

per cases by XXREAL_0:1;

case A45: i2 > j2 ; :: thesis:

then reconsider l = i2 - j2 as Element of NAT by INT_1:18;

A46: now

let n be Element of NAT ; :: thesis:
assume n in Seg l ; :: thesis:
then A47: ( 1 <= n & n <= l & 0 <= j2 ) by FINSEQ_1:3;
l <= i2 by XREAL_1:45;
then reconsider w = i2 - n as Element of NAT by A47, INT_1:18, XXREAL_0:2;
( 0 <= n & i2 - l <= i2 - n ) by A47, XREAL_1:15;
then ( i2 - n <= i2 & i2 <= width G & j2 <= w & 1 <= j2 ) by A28, FINSEQ_1:3, XREAL_1:45;
then ( 1 <= w & w <= width G ) by XXREAL_0:2;
then w in Seg (width G) by FINSEQ_1:3;
hence ( i2 - n is Element of NAT & [i1,(i2 - n)] in Indices G & i2 - n in Seg (width G) ) by A27, A28, ZFMISC_1:106; :: thesis:

end;

defpred S₃[ Nat, set ] means for m being Element of NAT st m = i2 - $1 holds
$2 = G * i1,m;

A48: now

let n be Nat; :: thesis:
assume n in Seg l ; :: thesis:
then reconsider m = i2 - n as Element of NAT by A46;
take p = G * i1,m; :: thesis:
thus S₃[n,p] ; :: thesis:

end;

consider g2 being FinSequence of (TOP-REAL 2) such that
A49: ( len g2 = l & ( for n being Nat st n in Seg l holds
S₃[n,g2 /. n] ) ) from FINSEQ_4:sch 1(A48);
A50: dom g2 = Seg l by A49, FINSEQ_1:def 3;
take g = g1 ^ g2; :: thesis:

now

let n be Element of NAT ; :: thesis:
assume A51: n in dom g2 ; :: thesis:
then reconsider m = i2 - n as Element of NAT by A46, A50;
take k = i1; :: thesis:
take m = m; :: thesis:
thus ( [k,m] in Indices G & g2 /. n = G * k,m ) by A46, A49, A50, A51; :: thesis:

end;

then A52: for n being Element of NAT st n in dom g holds
ex i, j being Element of NAT st
( [i,j] in Indices G & g /. n = G * i,j ) by A29, GOBOARD1:39;

A53: now

let n be Element of NAT ; :: thesis:
assume A54: ( n in dom g2 & n + 1 in dom g2 ) ; :: thesis:
then A55: ( i2 - n is Element of NAT & [i1,(i2 - n)] in Indices G & S₃[n,g2 /. n] & i2 - (n + 1) is Element of NAT & [i1,(i2 - (n + 1))] in Indices G & S₃[n + 1,g2 /. (n + 1)] ) by A46, A49, A50;
reconsider m1 = i2 - n, m2 = i2 - (n + 1) as Element of NAT by A46, A50, A54;
A56: ( g2 /. n = G * i1,m1 & g2 /. (n + 1) = G * i1,m2 ) by A49, A50, A54;
let l1, l2, l3, l4 be Element of NAT ; :: thesis:
assume ( [l1,l2] in Indices G & [l3,l4] in Indices G & g2 /. n = G * l1,l2 & g2 /. (n + 1) = G * l3,l4 ) ; :: thesis:
then ( l1 = i1 & l2 = m1 & l3 = i1 & l4 = m2 & 0 <= 1 ) by A55, A56, GOBOARD1:21;
hence (abs (l1 - l3)) + (abs (l2 - l4)) = 0 + (abs ((i2 - n) - (i2 - (n + 1)))) by ABSVALUE:7
.= 1 by ABSVALUE:def 1 ;
:: thesis:

end;

now

let l1, l2, l3, l4 be Element of NAT ; :: thesis:
assume A57: ( [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 ) ; :: thesis:
then A58: ( i2 - 1 is Element of NAT & [i1,(i2 - 1)] in Indices G & S₃[1,g2 /. 1] & (f | k) /. (len (f | k)) = f /. k ) by A14, A46, A49, A50, FINSEQ_4:86;
reconsider m1 = i2 - 1 as Element of NAT by A46, A50, A57;
g2 /. 1 = G * i1,m1 by A49, A50, A57;
then ( l1 = i1 & l2 = i2 & l3 = i1 & l4 = m1 & 0 <= 1 ) by A23, A24, A57, A58, GOBOARD1:21;
hence (abs (l1 - l3)) + (abs (l2 - l4)) = 0 + (abs (i2 - (i2 - 1))) by ABSVALUE:7
.= 1 by ABSVALUE:def 1 ;
:: thesis:

end;

then for n being Element of NAT st n in dom g & n + 1 in dom g holds
for m, k, i, j being Element of NAT st [m,k] in Indices G & [i,j] in Indices G & g /. n = G * m,k & g /. (n + 1) = G * i,j holds
(abs (m - i)) + (abs (k - j)) = 1 by A29, A53, GOBOARD1:40;
hence g is_sequence_on G by A52, GOBOARD1:def 11; :: thesis:
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 ) } ;
( i2 in dom l1 & j2 in dom l1 ) by A28, A39, FINSEQ_1:def 3;
then ( l1 /. i2 = l1 . i2 & l1 /. j2 = l1 . j2 ) by PARTFUN1:def 8;
then A59: ( l1 /. i2 = G * i1,i2 & l1 /. j2 = G * i1,j2 ) by A28, MATRIX_1:def 8;
then A60: ( (Y_axis l1) . i2 = (G * i1,i2) `2 & (Y_axis l1) . j2 = (G * i1,j2) `2 & (X_axis l1) . i2 = (G * i1,i2) `1 & (X_axis l1) . j2 = (G * i1,j2) `1 ) by A28, A35, A36, A37, A38, A39, GOBOARD1:def 3, GOBOARD1:def 4;
then A61: ( (G * i1,j2) `2 < (G * i1,i2) `2 & (G * i1,i2) `1 = (G * i1,j2) `1 & G * i1,i2 = |[((G * i1,i2) `1 ),((G * i1,i2) `2 )]| & G * i1,j2 = |[((G * i1,j2) `1 ),((G * i1,j2) `2 )]| ) by A28, A31, A32, A35, A36, A37, A38, A39, A45, EUCLID:57, GOBOARD1:def 2, SEQM_3:def 1;
A62: LSeg f,k = LSeg (G * i1,j2),(G * i1,i2) by A13, A24, A26, A44, TOPREAL1:def 5
.= { 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 A61, TOPREAL3:15 ;
thus L~ g = L~ f :: thesis:

proof

set lg = { (LSeg g,i) where i is Element of NAT : ( 1 <= i & i + 1 <= len g ) } ;
set lf = { (LSeg f,j) where j is Element of NAT : ( 1 <= j & j + 1 <= len f ) } ;
A63: len g = (len g1) + (len g2) by FINSEQ_1:35;

A64: now

let j be Element of NAT ; :: thesis:
assume A65: ( len g1 <= j & j <= len g ) ; :: thesis:
then reconsider w = j - (len g1) as Element of NAT by INT_1:18;
let p be Point of (TOP-REAL 2); :: thesis:
assume A66: p = g /. j ; :: thesis:
A67: dom l1 = Seg (len l1) by FINSEQ_1:def 3;

now

per cases ;

suppose A68: j = len g1 ; :: thesis:

1 <= len g1 by A13, A14, A23, XXREAL_0:2;
then len g1 in dom g1 by FINSEQ_3:27;
then A69: g /. (len g1) = (f | k) /. (len (f | k)) by A23, FINSEQ_4:83
.= G * i1,i2 by A14, A24, FINSEQ_4:86 ;
hence p `1 = (G * i1,i2) `1 by A66, A68; :: thesis:
thus ( (G * i1,j2) `2 <= p `2 & p `2 <= (G * i1,i2) `2 ) by A28, A32, A36, A37, A39, A45, A60, A66, A68, A69, SEQM_3:def 1; :: thesis:
thus p in rng l1 by A28, A39, A59, A66, A67, A68, A69, PARTFUN2:4; :: thesis:

end;

suppose A70: j <> len g1 ; :: thesis:

then A71: len g1 < j by A65, XXREAL_0:1;
j - (len g1) <> 0 by A70;
then A72: w >= 1 by NAT_1:14;
A73: w + (len g1) = j ;
then A74: w <= len g2 by A63, A65, XREAL_1:8;
then A75: ( (len g1) + 1 <= j & g /. j = g2 /. w ) by A71, A72, A73, Th5, NAT_1:13;
A76: w in dom g2 by A72, A74, FINSEQ_3:27;
then A77: ( i2 - w is Element of NAT & i2 - w in Seg (width G) & S₃[w,g2 /. w] ) by A46, A49, A50;
reconsider u = i2 - w as Element of NAT by A46, A50, A76;
u in dom l1 by A39, A77, FINSEQ_1:def 3;
then ( g2 /. w = g2 . w & l1 /. u = l1 . u ) by A76, PARTFUN1:def 8;
then A78: ( g2 /. w = G * i1,u & l1 /. u = G * i1,u ) by A77, MATRIX_1:def 8;
then A79: ( (X_axis l1) . i2 = (G * i1,i2) `1 & (X_axis l1) . u = (G * i1,u) `1 & (Y_axis l1) . i2 = (G * i1,i2) `2 & (Y_axis l1) . u = (G * i1,u) `2 & (Y_axis l1) . j2 = (G * i1,j2) `2 ) by A28, A35, A36, A37, A38, A39, A59, A77, GOBOARD1:def 3, GOBOARD1:def 4;
hence p `1 = (G * i1,i2) `1 by A28, A31, A35, A38, A39, A66, A75, A77, A78, GOBOARD1:def 2; :: thesis:

now

per cases ;

suppose u = j2 ; :: thesis:

hence (G * i1,j2) `2 <= p `2 by A66, A72, A73, A74, A78, Th5; :: thesis:

end;

suppose A80: u <> j2 ; :: thesis:

( i2 - (len g2) <= u & len g2 = l ) by A49, A74, XREAL_1:15;
then j2 < u by A80, XXREAL_0:1;
hence (G * i1,j2) `2 <= p `2 by A28, A32, A36, A37, A39, A66, A75, A77, A78, A79, SEQM_3:def 1; :: thesis:

end;

hence (G * i1,j2) `2 <= p `2 ; :: thesis:
u < i2 by A72, XREAL_1:46;
hence p `2 <= (G * i1,i2) `2 by A28, A32, A36, A37, A39, A66, A75, A77, A78, A79, SEQM_3:def 1; :: thesis:
thus p in rng l1 by A39, A66, A67, A75, A77, A78, PARTFUN2:4; :: thesis:

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:

end;

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

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in L~ g ; :: thesis:
then consider X being set such that
A81: ( x in X & X in { (LSeg g,i) where i is Element of NAT : ( 1 <= i & i + 1 <= len g ) } ) by TARSKI:def 4;
consider i being Element of NAT such that
A82: ( X = LSeg g,i & 1 <= i & i + 1 <= len g ) by A81;

now

per cases ;

suppose A83: i + 1 <= len g1 ; :: thesis:

then ( i <= i + 1 & i + 1 <= len g1 ) by NAT_1:11;
then ( 1 <= i & i <= len g1 & 1 <= i + 1 & i + 1 <= len g1 ) by A82, XXREAL_0:2;
then ( i in dom g1 & i + 1 in dom g1 ) by FINSEQ_3:27;
then X = LSeg g1,i by A82, TOPREAL3:25;
then X in { (LSeg g1,j) where j is Element of NAT : ( 1 <= j & j + 1 <= len g1 ) } by A82, A83;
then ( x in L~ (f | k) & L~ (f | k) c= L~ f ) by A23, A81, TARSKI:def 4, TOPREAL3:27;
hence x in L~ f ; :: thesis:

end;

suppose A84: i + 1 > len g1 ; :: thesis:

then A85: ( len g1 <= i & i <= i + 1 & i + 1 <= len g ) by A82, NAT_1:13;
A86: ( 1 <= i + 1 & len g1 <= i + 1 & i <= len g ) by A82, A84, NAT_1:13;
reconsider q1 = g /. i, q2 = g /. (i + 1) as Point of (TOP-REAL 2) ;
A87: ( q1 `1 = (G * i1,i2) `1 & (G * i1,j2) `2 <= q1 `2 & q1 `2 <= (G * i1,i2) `2 & q2 `1 = (G * i1,i2) `1 & (G * i1,j2) `2 <= q2 `2 & q2 `2 <= (G * i1,i2) `2 ) by A64, A85, A86;
then A88: ( q1 = |[(q1 `1 ),(q1 `2 )]| & q2 = |[(q1 `1 ),(q2 `2 )]| ) by EUCLID:57;
A89: LSeg g,i = LSeg q2,q1 by A82, TOPREAL1:def 5;

now

per cases by XXREAL_0:1;

suppose q1 `2 > q2 `2 ; :: thesis:

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 A88, A89, TOPREAL3:15;
then consider p2 being Point of (TOP-REAL 2) such that
A90: ( p2 = x & p2 `1 = q1 `1 & q2 `2 <= p2 `2 & p2 `2 <= q1 `2 ) by A81, A82;
( (G * i1,j2) `2 <= p2 `2 & p2 `2 <= (G * i1,i2) `2 ) by A87, A90, XXREAL_0:2;
then ( x in LSeg f,k & LSeg f,k in { (LSeg f,j) where j is Element of NAT : ( 1 <= j & j + 1 <= len f ) } ) by A13, A62, A87, A90;
hence x in L~ f by TARSKI:def 4; :: thesis:

end;

suppose q1 `2 = q2 `2 ; :: thesis:

then LSeg g,i = {q1} by A88, A89, RLTOPSP1:71;
then x = q1 by A81, A82, TARSKI:def 1;
then ( x in LSeg f,k & LSeg f,k in { (LSeg f,j) where j is Element of NAT : ( 1 <= j & j + 1 <= len f ) } ) by A13, A62, A87;
hence x in L~ f by TARSKI:def 4; :: thesis:

end;

suppose q1 `2 < q2 `2 ; :: thesis:

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 A88, A89, TOPREAL3:15;
then consider p2 being Point of (TOP-REAL 2) such that
A91: ( p2 = x & p2 `1 = q1 `1 & q1 `2 <= p2 `2 & p2 `2 <= q2 `2 ) by A81, A82;
( (G * i1,j2) `2 <= p2 `2 & p2 `2 <= (G * i1,i2) `2 ) by A87, A91, XXREAL_0:2;
then ( x in LSeg f,k & LSeg f,k in { (LSeg f,j) where j is Element of NAT : ( 1 <= j & j + 1 <= len f ) } ) by A13, A62, A87, A91;
hence x in L~ f by TARSKI:def 4; :: thesis:

end;

hence x in L~ f ; :: thesis:

end;

hence x in L~ f ; :: thesis:

end;

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in L~ f ; :: thesis:
then A92: x in (L~ (f | k)) \/ (LSeg f,k) by A5, A11, Th8;

now

per cases by A92, XBOOLE_0:def 3;

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

then ( x in L~ g1 & L~ g1 c= L~ g ) by A23, Th11;
hence x in L~ g ; :: thesis:

end;

suppose x in LSeg f,k ; :: thesis:

then consider p1 being Point of (TOP-REAL 2) such that
A93: ( p1 = x & p1 `1 = (G * i1,i2) `1 & (G * i1,j2) `2 <= p1 `2 & p1 `2 <= (G * i1,i2) `2 ) by A62;
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 ) );

A94: now

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

proof

thus ( len g1 <= n & n <= len g ) by A63, XREAL_1:33; :: thesis:
let q be Point of (TOP-REAL 2); :: thesis:
assume A95: q = g /. n ; :: thesis:
1 <= len g1 by A13, A14, A23, XXREAL_0:2;
then len g1 in dom g1 by FINSEQ_3:27;
then q = (f | k) /. (len (f | k)) by A23, A95, FINSEQ_4:83
.= G * i1,i2 by A14, A24, FINSEQ_4:86 ;
hence q `2 >= p1 `2 by A93; :: thesis:

end;

A96: for n being Nat st S₄[n] holds
n <= len g ;
consider ma being Nat such that
A97: ( S₄[ma] & ( for n being Nat st S₄[n] holds
n <= ma ) ) from NAT_1:sch 6(A96, A94);
reconsider ma = ma as Element of NAT by ORDINAL1:def 13;

now

per cases ;

suppose A98: ma = len g ; :: thesis:

j2 + 1 <= i2 by A45, NAT_1:13;
then A99: ( 1 <= l & l = len g2 ) by A49, XREAL_1:21;
then A100: ( l in dom g2 & i2 - l = j2 ) by A50, FINSEQ_1:3;
then A101: g /. ma = g2 /. l by A49, A63, A98, FINSEQ_4:84
.= G * i1,j2 by A49, A50, A100 ;
then p1 `2 <= (G * i1,j2) `2 by A97;
then A102: ( p1 `2 = (G * i1,j2) `2 & p1 = |[(p1 `1 ),(p1 `2 )]| ) by A93, EUCLID:57, XXREAL_0:1;
A103: ( ma <= (len g) + 1 & (len g1) + 1 <= ma & ma <= len g ) by A63, A98, A99, NAT_1:11, XREAL_1:9;
0 + 1 <= ma by A63, A98, A99, XREAL_1:9;
then reconsider m1 = ma - 1 as Element of NAT by INT_1:18;
A104: m1 + 1 = ma ;
then A105: m1 >= len g1 by A103, XREAL_1:8;
1 <= len g1 by A13, A14, A23, XXREAL_0:2;
then A106: 1 <= m1 by A105, XXREAL_0:2;
A107: m1 <= len g by A98, A104, NAT_1:11;
reconsider q = g /. m1 as Point of (TOP-REAL 2) ;
A108: q `1 = (G * i1,i2) `1 by A64, A105, A107;
A109: (G * i1,j2) `2 <= q `2 by A64, A105, A107;
A110: q = |[(q `1 ),(q `2 )]| by EUCLID:57;
A111: LSeg g,m1 = LSeg (G * i1,j2),q by A98, A101, A104, A106, TOPREAL1:def 5;
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 ) } ;
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 A61, A108, A109, A110, A111, TOPREAL3:15;
then ( p1 in LSeg g,m1 & LSeg g,m1 in { (LSeg g,i) where i is Element of NAT : ( 1 <= i & i + 1 <= len g ) } ) by A93, A98, A102, A104, A106, A109;
hence x in L~ g by A93, TARSKI:def 4; :: thesis:

end;

suppose ma <> len g ; :: thesis:

then ma < len g by A97, XXREAL_0:1;
then A112: ( 1 <= ma & ma + 1 <= len g & len g1 <= ma + 1 ) by A13, A14, A23, A97, NAT_1:13;
reconsider qa = g /. ma, qa1 = g /. (ma + 1) as Point of (TOP-REAL 2) ;
A113: p1 `2 <= qa `2 by A97;

A114: now

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

end;

then A115: ( qa1 `2 < qa `2 & qa1 `2 <= p1 `2 & p1 `2 <= qa `2 & qa `1 = (G * i1,i2) `1 & qa1 `1 = (G * i1,i2) `1 ) by A64, A97, A112, A113, XXREAL_0: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 ) } ;
A116: ( qa = |[(qa `1 ),(qa `2 )]| & qa1 = |[(qa1 `1 ),(qa1 `2 )]| ) by EUCLID:57;
LSeg g,ma = LSeg qa1,qa by A112, TOPREAL1:def 5
.= { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `1 = (G * i1,i2) `1 & qa1 `2 <= p2 `2 & p2 `2 <= qa `2 ) } by A115, A116, TOPREAL3:15 ;
then ( x in LSeg g,ma & LSeg g,ma in { (LSeg g,i) where i is Element of NAT : ( 1 <= i & i + 1 <= len g ) } ) by A93, A112, A113, A114;
hence x in L~ g by TARSKI:def 4; :: thesis:

end;

hence x in L~ g ; :: thesis:

end;

hence x in L~ g ; :: thesis:

end;

1 <= len g1 by A13, A14, A23, XXREAL_0:2;
then 1 in dom g1 by FINSEQ_3:27;
hence g /. 1 = (f | k) /. 1 by A23, FINSEQ_4:83
.= f /. 1 by A14, FINSEQ_4:86 ;
:: thesis:
j2 + 1 <= i2 by A45, NAT_1:13;
then A117: 1 <= l by XREAL_1:21;
then A118: ( l in dom g2 & len g = (len g1) + (len g2) & len g2 = l ) by A50, FINSEQ_1:3, FINSEQ_1:35, FINSEQ_1:def 3;
reconsider m1 = i2 - l as Element of NAT ;
thus g /. (len g) = g2 /. l by A118, FINSEQ_4:84
.= G * i1,m1 by A49, A50, A118
.= f /. (len f) by A5, A26, A44 ; :: thesis:
thus len f <= len g by A5, A14, A23, A117, A118, XREAL_1:9; :: thesis:

end;

case i2 = j2 ; :: thesis:

hence contradiction by A8, A14, A24, A25, A26, A44; :: thesis:

end;

case A119: i2 < j2 ; :: thesis:

then reconsider l = j2 - i2 as Element of NAT by INT_1:18;
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
A120: ( len g2 = l & ( for n being Nat st n in dom g2 holds
g2 /. n = H₁(n) ) ) from FINSEQ_4:sch 2();
A121: dom g2 = Seg l by A120, FINSEQ_1:def 3;
take g = g1 ^ g2; :: thesis:

A122: now

let n be Element of NAT ; :: thesis:
assume n in Seg l ; :: thesis:
then A123: ( 1 <= n & n <= l ) by FINSEQ_1:3;
then ( n <= n + i2 & i2 + n <= l + i2 ) by NAT_1:11, XREAL_1:9;
then ( n <= i2 + n & i2 + n <= j2 & j2 <= width G ) by A28, FINSEQ_1:3;
then ( 1 <= i2 + n & i2 + n <= width G ) by A123, XXREAL_0:2;
hence i2 + n in Seg (width G) by FINSEQ_1:3; :: thesis:
hence [i1,(i2 + n)] in Indices G by A27, A28, ZFMISC_1:106; :: thesis:

end;

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

now

let n be Element of NAT ; :: thesis:
assume A125: n in dom g2 ; :: thesis:
take m = i1; :: thesis:
take k = i2 + n; :: thesis:
thus ( [m,k] in Indices G & g2 /. n = G * m,k ) by A120, A122, A124, A125; :: thesis:

end;

then A126: for n being Element of NAT st n in dom g holds
ex i, j being Element of NAT st
( [i,j] in Indices G & g /. n = G * i,j ) by A29, GOBOARD1:39;

A127: now

let n be Element of NAT ; :: thesis:
assume ( n in dom g2 & n + 1 in dom g2 ) ; :: thesis:
then A128: ( g2 /. n = G * i1,(i2 + n) & [i1,(i2 + n)] in Indices G & g2 /. (n + 1) = G * i1,(i2 + (n + 1)) & [i1,(i2 + (n + 1))] in Indices G ) by A120, A122, A124;
let l1, l2, l3, l4 be Element of NAT ; :: thesis:
assume ( [l1,l2] in Indices G & [l3,l4] in Indices G & g2 /. n = G * l1,l2 & g2 /. (n + 1) = G * l3,l4 ) ; :: thesis:
then ( l1 = i1 & l2 = i2 + n & l3 = i1 & l4 = i2 + (n + 1) & 0 <= 1 ) by A128, GOBOARD1:21;
hence (abs (l1 - l3)) + (abs (l2 - l4)) = 0 + (abs ((i2 + n) - (i2 + (n + 1)))) by ABSVALUE:7
.= abs (- 1)
.= abs 1 by COMPLEX1:138
.= 1 by ABSVALUE:def 1 ;
:: thesis:

end;

now

let l1, l2, l3, l4 be Element of NAT ; :: thesis:
assume A129: ( [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 ) ; :: thesis:
then ( g2 /. 1 = G * i1,(i2 + 1) & [i1,(i2 + 1)] in Indices G & (f | k) /. (len (f | k)) = f /. k ) by A14, A120, A122, A124, FINSEQ_4:86;
then ( l1 = i1 & l2 = i2 & l3 = i1 & l4 = i2 + 1 & 0 <= 1 ) by A23, A24, A129, GOBOARD1:21;
hence (abs (l1 - l3)) + (abs (l2 - l4)) = 0 + (abs (i2 - (i2 + 1))) by ABSVALUE:7
.= abs ((i2 - i2) + (- 1))
.= abs 1 by COMPLEX1:138
.= 1 by ABSVALUE:def 1 ;
:: thesis:

end;

then for n being Element of NAT st n in dom g & n + 1 in dom g holds
for m, k, i, j being Element of NAT st [m,k] in Indices G & [i,j] in Indices G & g /. n = G * m,k & g /. (n + 1) = G * i,j holds
(abs (m - i)) + (abs (k - j)) = 1 by A29, A127, GOBOARD1:40;
hence g is_sequence_on G by A126, GOBOARD1:def 11; :: thesis:
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 ) } ;
( i2 in dom l1 & j2 in dom l1 ) by A28, A39, FINSEQ_1:def 3;
then ( l1 /. i2 = l1 . i2 & l1 /. j2 = l1 . j2 ) by PARTFUN1:def 8;
then A130: ( l1 /. i2 = G * i1,i2 & l1 /. j2 = G * i1,j2 ) by A28, MATRIX_1:def 8;
then A131: ( (Y_axis l1) . i2 = (G * i1,i2) `2 & (Y_axis l1) . j2 = (G * i1,j2) `2 & (X_axis l1) . i2 = (G * i1,i2) `1 & (X_axis l1) . j2 = (G * i1,j2) `1 ) by A28, A35, A36, A37, A38, A39, GOBOARD1:def 3, GOBOARD1:def 4;
then A132: ( (G * i1,i2) `2 < (G * i1,j2) `2 & (G * i1,i2) `1 = (G * i1,j2) `1 & G * i1,i2 = |[((G * i1,i2) `1 ),((G * i1,i2) `2 )]| & G * i1,j2 = |[((G * i1,j2) `1 ),((G * i1,j2) `2 )]| ) by A28, A31, A32, A35, A36, A37, A38, A39, A119, EUCLID:57, GOBOARD1:def 2, SEQM_3:def 1;
A133: LSeg f,k = LSeg (G * i1,i2),(G * i1,j2) by A13, A24, A26, A44, TOPREAL1:def 5
.= { 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 A132, TOPREAL3:15 ;
thus L~ g = L~ f :: thesis:

proof

set lg = { (LSeg g,i) where i is Element of NAT : ( 1 <= i & i + 1 <= len g ) } ;
set lf = { (LSeg f,j) where j is Element of NAT : ( 1 <= j & j + 1 <= len f ) } ;
A134: len g = (len g1) + (len g2) by FINSEQ_1:35;

A135: now

let j be Element of NAT ; :: thesis:
assume A136: ( len g1 <= j & j <= len g ) ; :: thesis:
then reconsider w = j - (len g1) as Element of NAT by INT_1:18;
let p be Point of (TOP-REAL 2); :: thesis:
assume A137: p = g /. j ; :: thesis:
set u = i2 + w;
A138: dom l1 = Seg (len l1) by FINSEQ_1:def 3;

now

per cases ;

suppose A139: j = len g1 ; :: thesis:

1 <= len g1 by A13, A14, A23, XXREAL_0:2;
then len g1 in dom g1 by FINSEQ_3:27;
then A140: g /. (len g1) = (f | k) /. (len (f | k)) by A23, FINSEQ_4:83
.= G * i1,i2 by A14, A24, FINSEQ_4:86 ;
hence p `1 = (G * i1,i2) `1 by A137, A139; :: thesis:
thus ( (G * i1,i2) `2 <= p `2 & p `2 <= (G * i1,j2) `2 ) by A28, A32, A36, A37, A39, A119, A131, A137, A139, A140, SEQM_3:def 1; :: thesis:
thus p in rng l1 by A28, A39, A130, A137, A138, A139, A140, PARTFUN2:4; :: thesis:

end;

suppose A141: j <> len g1 ; :: thesis:

then A142: len g1 < j by A136, XXREAL_0:1;
A143: j - (len g1) <> 0 by A141;
then A144: w >= 1 by NAT_1:14;
A145: w + (len g1) = j ;
then A146: w <= len g2 by A134, A136, XREAL_1:8;
then A147: ( (len g1) + 1 <= j & g /. j = g2 /. w ) by A142, A144, A145, Th5, NAT_1:13;
A148: w in dom g2 by A144, A146, FINSEQ_3:27;
then i2 + w in Seg (width G) by A121, A122;
then i2 + w in dom l1 by A39, FINSEQ_1:def 3;
then A149: ( g2 /. w = g2 . w & l1 /. (i2 + w) = l1 . (i2 + w) ) by A148, PARTFUN1:def 8;
A150: ( g2 /. w = G * i1,(i2 + w) & i2 + w in Seg (width G) ) by A120, A121, A122, A148;
then A151: l1 /. (i2 + w) = G * i1,(i2 + w) by A149, MATRIX_1:def 8;
then A152: ( (X_axis l1) . i2 = (G * i1,i2) `1 & (X_axis l1) . (i2 + w) = (G * i1,(i2 + w)) `1 & (Y_axis l1) . i2 = (G * i1,i2) `2 & (Y_axis l1) . (i2 + w) = (G * i1,(i2 + w)) `2 & (Y_axis l1) . j2 = (G * i1,j2) `2 ) by A28, A35, A36, A37, A38, A39, A130, A150, GOBOARD1:def 3, GOBOARD1:def 4;
hence p `1 = (G * i1,i2) `1 by A28, A31, A35, A38, A39, A137, A147, A150, GOBOARD1:def 2; :: thesis:
0 + 1 <= w by A143, NAT_1:14;
then i2 < i2 + w by XREAL_1:31;
hence (G * i1,i2) `2 <= p `2 by A28, A32, A36, A37, A39, A137, A147, A150, A152, SEQM_3:def 1; :: thesis:

now

per cases ;

suppose i2 + w = j2 ; :: thesis:

hence p `2 <= (G * i1,j2) `2 by A137, A144, A145, A146, A150, Th5; :: thesis:

end;

suppose A153: i2 + w <> j2 ; :: thesis:

i2 + w <= i2 + l by A120, A146, XREAL_1:9;
then i2 + w < j2 by A153, XXREAL_0:1;
hence p `2 <= (G * i1,j2) `2 by A28, A32, A36, A37, A39, A137, A147, A150, A152, SEQM_3:def 1; :: thesis:

end;

hence p `2 <= (G * i1,j2) `2 ; :: thesis:
thus p in rng l1 by A39, A137, A138, A147, A150, A151, PARTFUN2:4; :: thesis:

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:

end;

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

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in L~ g ; :: thesis:
then consider X being set such that
A154: ( x in X & X in { (LSeg g,i) where i is Element of NAT : ( 1 <= i & i + 1 <= len g ) } ) by TARSKI:def 4;
consider i being Element of NAT such that
A155: ( X = LSeg g,i & 1 <= i & i + 1 <= len g ) by A154;

now

per cases ;

suppose A156: i + 1 <= len g1 ; :: thesis:

then ( i <= i + 1 & i + 1 <= len g1 ) by NAT_1:11;
then ( 1 <= i & i <= len g1 & 1 <= i + 1 & i + 1 <= len g1 ) by A155, XXREAL_0:2;
then ( i in dom g1 & i + 1 in dom g1 ) by FINSEQ_3:27;
then X = LSeg g1,i by A155, TOPREAL3:25;
then X in { (LSeg g1,j) where j is Element of NAT : ( 1 <= j & j + 1 <= len g1 ) } by A155, A156;
then ( x in L~ (f | k) & L~ (f | k) c= L~ f ) by A23, A154, TARSKI:def 4, TOPREAL3:27;
hence x in L~ f ; :: thesis:

end;

suppose A157: i + 1 > len g1 ; :: thesis:

then A158: ( len g1 <= i & i <= i + 1 & i + 1 <= len g ) by A155, NAT_1:13;
A159: ( 1 <= i + 1 & len g1 <= i + 1 & i <= len g ) by A155, A157, NAT_1:13;
reconsider q1 = g /. i, q2 = g /. (i + 1) as Point of (TOP-REAL 2) ;
A160: ( q1 `1 = (G * i1,i2) `1 & (G * i1,i2) `2 <= q1 `2 & q1 `2 <= (G * i1,j2) `2 & q2 `1 = (G * i1,i2) `1 & (G * i1,i2) `2 <= q2 `2 & q2 `2 <= (G * i1,j2) `2 ) by A135, A158, A159;
then A161: ( q1 = |[(q1 `1 ),(q1 `2 )]| & q2 = |[(q1 `1 ),(q2 `2 )]| ) by EUCLID:57;
A162: LSeg g,i = LSeg q2,q1 by A155, TOPREAL1:def 5;

now

per cases by XXREAL_0:1;

suppose q1 `2 > q2 `2 ; :: thesis:

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 A161, A162, TOPREAL3:15;
then consider p2 being Point of (TOP-REAL 2) such that
A163: ( p2 = x & p2 `1 = q1 `1 & q2 `2 <= p2 `2 & p2 `2 <= q1 `2 ) by A154, A155;
( (G * i1,i2) `2 <= p2 `2 & p2 `2 <= (G * i1,j2) `2 ) by A160, A163, XXREAL_0:2;
then ( x in LSeg f,k & LSeg f,k in { (LSeg f,j) where j is Element of NAT : ( 1 <= j & j + 1 <= len f ) } ) by A13, A133, A160, A163;
hence x in L~ f by TARSKI:def 4; :: thesis:

end;

suppose q1 `2 = q2 `2 ; :: thesis:

then LSeg g,i = {q1} by A161, A162, RLTOPSP1:71;
then x = q1 by A154, A155, TARSKI:def 1;
then ( x in LSeg f,k & LSeg f,k in { (LSeg f,j) where j is Element of NAT : ( 1 <= j & j + 1 <= len f ) } ) by A13, A133, A160;
hence x in L~ f by TARSKI:def 4; :: thesis:

end;

suppose q1 `2 < q2 `2 ; :: thesis:

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 A161, A162, TOPREAL3:15;
then consider p2 being Point of (TOP-REAL 2) such that
A164: ( p2 = x & p2 `1 = q1 `1 & q1 `2 <= p2 `2 & p2 `2 <= q2 `2 ) by A154, A155;
( (G * i1,i2) `2 <= p2 `2 & p2 `2 <= (G * i1,j2) `2 ) by A160, A164, XXREAL_0:2;
then ( x in LSeg f,k & LSeg f,k in { (LSeg f,j) where j is Element of NAT : ( 1 <= j & j + 1 <= len f ) } ) by A13, A133, A160, A164;
hence x in L~ f by TARSKI:def 4; :: thesis:

end;

hence x in L~ f ; :: thesis:

end;

hence x in L~ f ; :: thesis:

end;

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in L~ f ; :: thesis:
then A165: x in (L~ (f | k)) \/ (LSeg f,k) by A5, A11, Th8;

now

per cases by A165, XBOOLE_0:def 3;

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

then ( x in L~ g1 & L~ g1 c= L~ g ) by A23, Th11;
hence x in L~ g ; :: thesis:

end;

suppose x in LSeg f,k ; :: thesis:

then consider p1 being Point of (TOP-REAL 2) such that
A166: ( p1 = x & p1 `1 = (G * i1,i2) `1 & (G * i1,i2) `2 <= p1 `2 & p1 `2 <= (G * i1,j2) `2 ) by A133;
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 ) );

A167: now

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

proof

thus ( len g1 <= n & n <= len g ) by A134, XREAL_1:33; :: thesis:
let q be Point of (TOP-REAL 2); :: thesis:
assume A168: q = g /. n ; :: thesis:
1 <= len g1 by A13, A14, A23, XXREAL_0:2;
then len g1 in dom g1 by FINSEQ_3:27;
then q = (f | k) /. (len (f | k)) by A23, A168, FINSEQ_4:83
.= G * i1,i2 by A14, A24, FINSEQ_4:86 ;
hence q `2 <= p1 `2 by A166; :: thesis:

end;

A169: for n being Nat st S₃[n] holds
n <= len g ;
consider ma being Nat such that
A170: ( S₃[ma] & ( for n being Nat st S₃[n] holds
n <= ma ) ) from NAT_1:sch 6(A169, A167);
reconsider ma = ma as Element of NAT by ORDINAL1:def 13;

now

per cases ;

suppose A171: ma = len g ; :: thesis:

i2 + 1 <= j2 by A119, NAT_1:13;
then A172: 1 <= l by XREAL_1:21;
then A173: ( l in dom g2 & i2 + l = j2 ) by A120, FINSEQ_3:27;
then A174: g /. ma = g2 /. l by A120, A134, A171, FINSEQ_4:84
.= G * i1,j2 by A120, A173 ;
then (G * i1,j2) `2 <= p1 `2 by A170;
then A175: ( p1 `2 = (G * i1,j2) `2 & p1 = |[(p1 `1 ),(p1 `2 )]| ) by A166, EUCLID:57, XXREAL_0:1;
A176: ( ma <= (len g) + 1 & (len g1) + 1 <= ma & ma <= len g ) by A120, A134, A171, A172, NAT_1:11, XREAL_1:9;
0 + 1 <= ma by A120, A134, A171, A172, XREAL_1:9;
then reconsider m1 = ma - 1 as Element of NAT by INT_1:18;
A177: m1 + 1 = ma ;
then A178: m1 >= len g1 by A176, XREAL_1:8;
1 <= len g1 by A13, A14, A23, XXREAL_0:2;
then A179: 1 <= m1 by A178, XXREAL_0:2;
A180: m1 <= len g by A171, A177, NAT_1:11;
reconsider q = g /. m1 as Point of (TOP-REAL 2) ;
A181: q `1 = (G * i1,i2) `1 by A135, A178, A180;
A182: q `2 <= (G * i1,j2) `2 by A135, A178, A180;
A183: q = |[(q `1 ),(q `2 )]| by EUCLID:57;
A184: LSeg g,m1 = LSeg (G * i1,j2),q by A171, A174, A177, A179, TOPREAL1:def 5;
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 ) } ;
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 A132, A181, A182, A183, A184, TOPREAL3:15;
then ( p1 in LSeg g,m1 & LSeg g,m1 in { (LSeg g,i) where i is Element of NAT : ( 1 <= i & i + 1 <= len g ) } ) by A166, A171, A175, A177, A179, A182;
hence x in L~ g by A166, TARSKI:def 4; :: thesis:

end;

suppose ma <> len g ; :: thesis:

then ma < len g by A170, XXREAL_0:1;
then A185: ( 1 <= ma & ma + 1 <= len g & len g1 <= ma + 1 ) by A13, A14, A23, A170, NAT_1:13;
reconsider qa = g /. ma, qa1 = g /. (ma + 1) as Point of (TOP-REAL 2) ;
A186: qa `2 <= p1 `2 by A170;

A187: now

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

end;

then A188: ( qa `2 < qa1 `2 & qa `2 <= p1 `2 & p1 `2 <= qa1 `2 & qa `1 = (G * i1,i2) `1 & qa1 `1 = (G * i1,i2) `1 ) by A135, A170, A185, A186, XXREAL_0: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 ) } ;
A189: ( qa = |[(qa `1 ),(qa `2 )]| & qa1 = |[(qa1 `1 ),(qa1 `2 )]| ) by EUCLID:57;
LSeg g,ma = LSeg qa,qa1 by A185, TOPREAL1:def 5
.= { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `1 = (G * i1,i2) `1 & qa `2 <= p2 `2 & p2 `2 <= qa1 `2 ) } by A188, A189, TOPREAL3:15 ;
then ( x in LSeg g,ma & LSeg g,ma in { (LSeg g,i) where i is Element of NAT : ( 1 <= i & i + 1 <= len g ) } ) by A166, A185, A186, A187;
hence x in L~ g by TARSKI:def 4; :: thesis:

end;

hence x in L~ g ; :: thesis:

end;

hence x in L~ g ; :: thesis:

end;

1 <= len g1 by A13, A14, A23, XXREAL_0:2;
then 1 in dom g1 by FINSEQ_3:27;
hence g /. 1 = (f | k) /. 1 by A23, FINSEQ_4:83
.= f /. 1 by A14, FINSEQ_4:86 ;
:: thesis:
i2 + 1 <= j2 by A119, NAT_1:13;
then A190: 1 <= l by XREAL_1:21;
then A191: ( l in dom g2 & len g = (len g1) + l ) by A120, A124, FINSEQ_1:3, FINSEQ_1:35;
hence g /. (len g) = g2 /. l by FINSEQ_4:84
.= G * i1,(i2 + l) by A120, A191
.= f /. (len f) by A5, A26, A44 ;
:: thesis:
thus len f <= len g by A5, A14, A23, A190, A191, XREAL_1:9; :: thesis:

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:

end;

suppose A192: i2 = j2 ; :: thesis:

set ppi = G * i1,i2;
set pj = G * j1,i2;

now

per cases by XXREAL_0:1;

case A193: i1 > j1 ; :: thesis:

then reconsider l = i1 - j1 as Element of NAT by INT_1:18;

A194: now

let n be Element of NAT ; :: thesis:
assume n in Seg l ; :: thesis:
then A195: ( 1 <= n & n <= l & 0 <= j1 ) by FINSEQ_1:3;
l <= i1 by XREAL_1:45;
then reconsider w = i1 - n as Element of NAT by A195, INT_1:18, XXREAL_0:2;
( 0 <= n & i1 - l <= i1 - n ) by A195, XREAL_1:15;
then ( i1 - n <= i1 & i1 <= len G & j1 <= w & 1 <= j1 ) by A28, FINSEQ_3:27, XREAL_1:45;
then ( 1 <= w & w <= len G ) by XXREAL_0:2;
then w in dom G by FINSEQ_3:27;
hence ( i1 - n is Element of NAT & [(i1 - n),i2] in Indices G & i1 - n in dom G ) by A27, A28, ZFMISC_1:106; :: thesis:

end;

defpred S₃[ Nat, set ] means for m being Element of NAT st m = i1 - $1 holds
$2 = G * m,i2;

A196: now

let n be Nat; :: thesis:
assume n in Seg l ; :: thesis:
then reconsider m = i1 - n as Element of NAT by A194;
take p = G * m,i2; :: thesis:
thus S₃[n,p] ; :: thesis:

end;

consider g2 being FinSequence of (TOP-REAL 2) such that
A197: ( len g2 = l & ( for n being Nat st n in Seg l holds
S₃[n,g2 /. n] ) ) from FINSEQ_4:sch 1(A196);
A198: dom g2 = Seg l by A197, FINSEQ_1:def 3;
take g = g1 ^ g2; :: thesis:

now

let n be Element of NAT ; :: thesis:
assume A199: n in dom g2 ; :: thesis:
then reconsider m = i1 - n as Element of NAT by A194, A198;
take m = m; :: thesis:
take k = i2; :: thesis:
thus ( [m,k] in Indices G & g2 /. n = G * m,k ) by A194, A197, A198, A199; :: thesis:

end;

then A200: for n being Element of NAT st n in dom g holds
ex i, j being Element of NAT st
( [i,j] in Indices G & g /. n = G * i,j ) by A29, GOBOARD1:39;

A201: now

let n be Element of NAT ; :: thesis:
assume A202: ( n in dom g2 & n + 1 in dom g2 ) ; :: thesis:
then A203: ( i1 - n is Element of NAT & [(i1 - n),i2] in Indices G & S₃[n,g2 /. n] & i1 - (n + 1) is Element of NAT & [(i1 - (n + 1)),i2] in Indices G & S₃[n + 1,g2 /. (n + 1)] ) by A194, A197, A198;
reconsider m1 = i1 - n, m2 = i1 - (n + 1) as Element of NAT by A194, A198, A202;
A204: ( g2 /. n = G * m1,i2 & g2 /. (n + 1) = G * m2,i2 ) by A197, A198, A202;
let l1, l2, l3, l4 be Element of NAT ; :: thesis:
assume ( [l1,l2] in Indices G & [l3,l4] in Indices G & g2 /. n = G * l1,l2 & g2 /. (n + 1) = G * l3,l4 ) ; :: thesis:
then ( l1 = m1 & l2 = i2 & l3 = m2 & l4 = i2 & 0 <= 1 ) by A203, A204, GOBOARD1:21;
hence (abs (l1 - l3)) + (abs (l2 - l4)) = (abs ((i1 - n) - (i1 - (n + 1)))) + 0 by ABSVALUE:7
.= 1 by ABSVALUE:def 1 ;
:: thesis:

end;

now

let l1, l2, l3, l4 be Element of NAT ; :: thesis:
assume A205: ( [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 ) ; :: thesis:
then A206: ( i1 - 1 is Element of NAT & [(i1 - 1),i2] in Indices G & S₃[1,g2 /. 1] & (f | k) /. (len (f | k)) = f /. k ) by A14, A194, A197, A198, FINSEQ_4:86;
reconsider m1 = i1 - 1 as Element of NAT by A194, A198, A205;
g2 /. 1 = G * m1,i2 by A197, A198, A205;
then ( l1 = i1 & l2 = i2 & l3 = m1 & l4 = i2 & 0 <= 1 ) by A23, A24, A205, A206, GOBOARD1:21;
hence (abs (l1 - l3)) + (abs (l2 - l4)) = (abs (i1 - (i1 - 1))) + 0 by ABSVALUE:7
.= 1 by ABSVALUE:def 1 ;
:: thesis:

end;

then for n being Element of NAT st n in dom g & n + 1 in dom g holds
for m, k, i, j being Element of NAT st [m,k] in Indices G & [i,j] in Indices G & g /. n = G * m,k & g /. (n + 1) = G * i,j holds
(abs (m - i)) + (abs (k - j)) = 1 by A29, A201, GOBOARD1:40;
hence g is_sequence_on G by A200, GOBOARD1:def 11; :: thesis:
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 ) } ;
( c1 /. i1 = c1 . i1 & c1 /. j1 = c1 . j1 ) by A28, A42, PARTFUN1:def 8;
then A207: ( c1 /. i1 = G * i1,i2 & c1 /. j1 = G * j1,i2 ) by A28, MATRIX_1:def 9;
then A208: ( (Y_axis c1) . i1 = (G * i1,i2) `2 & (Y_axis c1) . j1 = (G * j1,i2) `2 & (X_axis c1) . i1 = (G * i1,i2) `1 & (X_axis c1) . j1 = (G * j1,i2) `1 ) by A28, A42, A43, GOBOARD1:def 3, GOBOARD1:def 4;
then A209: ( (G * j1,i2) `1 < (G * i1,i2) `1 & (G * i1,i2) `2 = (G * j1,i2) `2 & G * i1,i2 = |[((G * i1,i2) `1 ),((G * i1,i2) `2 )]| & G * j1,i2 = |[((G * j1,i2) `1 ),((G * j1,i2) `2 )]| ) by A28, A33, A34, A42, A43, A193, EUCLID:57, GOBOARD1:def 2, SEQM_3:def 1;
A210: LSeg f,k = LSeg (G * j1,i2),(G * i1,i2) by A13, A24, A26, A192, TOPREAL1:def 5
.= { 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 A209, TOPREAL3:16 ;
thus L~ g = L~ f :: thesis:

proof

set lg = { (LSeg g,i) where i is Element of NAT : ( 1 <= i & i + 1 <= len g ) } ;
set lf = { (LSeg f,j) where j is Element of NAT : ( 1 <= j & j + 1 <= len f ) } ;
A211: len g = (len g1) + (len g2) by FINSEQ_1:35;

A212: now

let j be Element of NAT ; :: thesis:
assume A213: ( len g1 <= j & j <= len g ) ; :: thesis:
then reconsider w = j - (len g1) as Element of NAT by INT_1:18;
let p be Point of (TOP-REAL 2); :: thesis:
assume A214: p = g /. j ; :: thesis:

now

per cases ;

suppose A215: j = len g1 ; :: thesis:

1 <= len g1 by A13, A14, A23, XXREAL_0:2;
then len g1 in dom g1 by FINSEQ_3:27;
then A216: g /. (len g1) = (f | k) /. (len (f | k)) by A23, FINSEQ_4:83
.= G * i1,i2 by A14, A24, FINSEQ_4:86 ;
hence p `2 = (G * i1,i2) `2 by A214, A215; :: thesis:
thus ( (G * j1,i2) `1 <= p `1 & p `1 <= (G * i1,i2) `1 ) by A28, A33, A42, A43, A193, A208, A214, A215, A216, SEQM_3:def 1; :: thesis:
thus p in rng c1 by A28, A42, A207, A214, A215, A216, PARTFUN2:4; :: thesis:

end;

suppose A217: j <> len g1 ; :: thesis:

then A218: len g1 < j by A213, XXREAL_0:1;
j - (len g1) <> 0 by A217;
then A219: w >= 1 by NAT_1:14;
A220: w + (len g1) = j ;
then A221: w <= len g2 by A211, A213, XREAL_1:8;
then A222: ( (len g1) + 1 <= j & g /. j = g2 /. w ) by A218, A219, A220, Th5, NAT_1:13;
A223: w in dom g2 by A219, A221, FINSEQ_3:27;
then A224: ( i1 - w is Element of NAT & i1 - w in dom G & S₃[w,g2 /. w] ) by A194, A197, A198;
reconsider u = i1 - w as Element of NAT by A194, A198, A223;
( g2 /. w = g2 . w & c1 /. u = c1 . u ) by A42, A223, A224, PARTFUN1:def 8;
then A225: ( g2 /. w = G * u,i2 & c1 /. u = G * u,i2 ) by A224, MATRIX_1:def 9;
then A226: ( (X_axis c1) . i1 = (G * i1,i2) `1 & (X_axis c1) . u = (G * u,i2) `1 & (X_axis c1) . j1 = (G * j1,i2) `1 & (Y_axis c1) . i1 = (G * i1,i2) `2 & (Y_axis c1) . u = (G * u,i2) `2 & (Y_axis c1) . j1 = (G * j1,i2) `2 ) by A28, A42, A43, A207, A224, GOBOARD1:def 3, GOBOARD1:def 4;
hence p `2 = (G * i1,i2) `2 by A28, A34, A42, A43, A214, A222, A224, A225, GOBOARD1:def 2; :: thesis:

now

per cases ;

suppose u = j1 ; :: thesis:

hence (G * j1,i2) `1 <= p `1 by A214, A219, A220, A221, A225, Th5; :: thesis:

end;

suppose A227: u <> j1 ; :: thesis:

( i1 - (len g2) <= u & len g2 = l ) by A197, A221, XREAL_1:15;
then j1 < u by A227, XXREAL_0:1;
hence (G * j1,i2) `1 <= p `1 by A28, A33, A42, A43, A214, A222, A224, A225, A226, SEQM_3:def 1; :: thesis:

end;

hence (G * j1,i2) `1 <= p `1 ; :: thesis:
u < i1 by A219, XREAL_1:46;
hence p `1 <= (G * i1,i2) `1 by A28, A33, A42, A43, A214, A222, A224, A225, A226, SEQM_3:def 1; :: thesis:
thus p in rng c1 by A42, A214, A222, A224, A225, PARTFUN2:4; :: thesis:

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:

end;

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

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in L~ g ; :: thesis:
then consider X being set such that
A228: ( x in X & X in { (LSeg g,i) where i is Element of NAT : ( 1 <= i & i + 1 <= len g ) } ) by TARSKI:def 4;
consider i being Element of NAT such that
A229: ( X = LSeg g,i & 1 <= i & i + 1 <= len g ) by A228;

now

per cases ;

suppose A230: i + 1 <= len g1 ; :: thesis:

then ( i <= i + 1 & i + 1 <= len g1 ) by NAT_1:11;
then ( 1 <= i & i <= len g1 & 1 <= i + 1 & i + 1 <= len g1 ) by A229, XXREAL_0:2;
then ( i in dom g1 & i + 1 in dom g1 ) by FINSEQ_3:27;
then X = LSeg g1,i by A229, TOPREAL3:25;
then X in { (LSeg g1,j) where j is Element of NAT : ( 1 <= j & j + 1 <= len g1 ) } by A229, A230;
then ( x in L~ (f | k) & L~ (f | k) c= L~ f ) by A23, A228, TARSKI:def 4, TOPREAL3:27;
hence x in L~ f ; :: thesis:

end;

suppose A231: i + 1 > len g1 ; :: thesis:

then A232: ( len g1 <= i & i <= i + 1 & i + 1 <= len g ) by A229, NAT_1:13;
A233: ( 1 <= i + 1 & len g1 <= i + 1 & i <= len g ) by A229, A231, NAT_1:13;
reconsider q1 = g /. i, q2 = g /. (i + 1) as Point of (TOP-REAL 2) ;
A234: ( q1 `2 = (G * i1,i2) `2 & (G * j1,i2) `1 <= q1 `1 & q1 `1 <= (G * i1,i2) `1 & q2 `2 = (G * i1,i2) `2 & (G * j1,i2) `1 <= q2 `1 & q2 `1 <= (G * i1,i2) `1 ) by A212, A232, A233;
then A235: ( q1 = |[(q1 `1 ),(q1 `2 )]| & q2 = |[(q2 `1 ),(q1 `2 )]| ) by EUCLID:57;
A236: LSeg g,i = LSeg q2,q1 by A229, TOPREAL1:def 5;

now

per cases by XXREAL_0:1;

suppose q1 `1 > q2 `1 ; :: thesis:

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 A235, A236, TOPREAL3:16;
then consider p2 being Point of (TOP-REAL 2) such that
A237: ( p2 = x & p2 `2 = q1 `2 & q2 `1 <= p2 `1 & p2 `1 <= q1 `1 ) by A228, A229;
( (G * j1,i2) `1 <= p2 `1 & p2 `1 <= (G * i1,i2) `1 ) by A234, A237, XXREAL_0:2;
then ( x in LSeg f,k & LSeg f,k in { (LSeg f,j) where j is Element of NAT : ( 1 <= j & j + 1 <= len f ) } ) by A13, A210, A234, A237;
hence x in L~ f by TARSKI:def 4; :: thesis:

end;

suppose q1 `1 = q2 `1 ; :: thesis:

then LSeg g,i = {q1} by A235, A236, RLTOPSP1:71;
then x = q1 by A228, A229, TARSKI:def 1;
then ( x in LSeg f,k & LSeg f,k in { (LSeg f,j) where j is Element of NAT : ( 1 <= j & j + 1 <= len f ) } ) by A13, A210, A234;
hence x in L~ f by TARSKI:def 4; :: thesis:

end;

suppose q1 `1 < q2 `1 ; :: thesis:

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 A235, A236, TOPREAL3:16;
then consider p2 being Point of (TOP-REAL 2) such that
A238: ( p2 = x & p2 `2 = q1 `2 & q1 `1 <= p2 `1 & p2 `1 <= q2 `1 ) by A228, A229;
( (G * j1,i2) `1 <= p2 `1 & p2 `1 <= (G * i1,i2) `1 ) by A234, A238, XXREAL_0:2;
then ( x in LSeg f,k & LSeg f,k in { (LSeg f,j) where j is Element of NAT : ( 1 <= j & j + 1 <= len f ) } ) by A13, A210, A234, A238;
hence x in L~ f by TARSKI:def 4; :: thesis:

end;

hence x in L~ f ; :: thesis:

end;

hence x in L~ f ; :: thesis:

end;

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in L~ f ; :: thesis:
then A239: x in (L~ (f | k)) \/ (LSeg f,k) by A5, A11, Th8;

now

per cases by A239, XBOOLE_0:def 3;

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

then ( x in L~ g1 & L~ g1 c= L~ g ) by A23, Th11;
hence x in L~ g ; :: thesis:

end;

suppose x in LSeg f,k ; :: thesis:

then consider p1 being Point of (TOP-REAL 2) such that
A240: ( p1 = x & p1 `2 = (G * i1,i2) `2 & (G * j1,i2) `1 <= p1 `1 & p1 `1 <= (G * i1,i2) `1 ) by A210;
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 ) );

A241: now

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

proof

thus ( len g1 <= n & n <= len g ) by A211, XREAL_1:33; :: thesis:
let q be Point of (TOP-REAL 2); :: thesis:
assume A242: q = g /. n ; :: thesis:
1 <= len g1 by A13, A14, A23, XXREAL_0:2;
then len g1 in dom g1 by FINSEQ_3:27;
then q = (f | k) /. (len (f | k)) by A23, A242, FINSEQ_4:83
.= G * i1,i2 by A14, A24, FINSEQ_4:86 ;
hence q `1 >= p1 `1 by A240; :: thesis:

end;

A243: for n being Nat st S₄[n] holds
n <= len g ;
consider ma being Nat such that
A244: ( S₄[ma] & ( for n being Nat st S₄[n] holds
n <= ma ) ) from NAT_1:sch 6(A243, A241);
reconsider ma = ma as Element of NAT by ORDINAL1:def 13;

now

per cases ;

suppose A245: ma = len g ; :: thesis:

j1 + 1 <= i1 by A193, NAT_1:13;
then A246: ( 1 <= l & l = len g2 ) by A197, XREAL_1:21;
then A247: ( l in dom g2 & i1 - l = j1 ) by A198, FINSEQ_1:3;
then A248: g /. ma = g2 /. l by A197, A211, A245, FINSEQ_4:84
.= G * j1,i2 by A197, A198, A247 ;
then p1 `1 <= (G * j1,i2) `1 by A244;
then A249: ( p1 `1 = (G * j1,i2) `1 & p1 = |[(p1 `1 ),(p1 `2 )]| ) by A240, EUCLID:57, XXREAL_0:1;
A250: ( ma <= (len g) + 1 & (len g1) + 1 <= ma & ma <= len g ) by A211, A245, A246, NAT_1:11, XREAL_1:9;
0 + 1 <= ma by A211, A245, A246, XREAL_1:9;
then reconsider m1 = ma - 1 as Element of NAT by INT_1:18;
A251: m1 + 1 = ma ;
then A252: m1 >= len g1 by A250, XREAL_1:8;
1 <= len g1 by A13, A14, A23, XXREAL_0:2;
then A253: 1 <= m1 by A252, XXREAL_0:2;
A254: m1 <= len g by A245, A251, NAT_1:11;
reconsider q = g /. m1 as Point of (TOP-REAL 2) ;
A255: q `2 = (G * i1,i2) `2 by A212, A252, A254;
A256: (G * j1,i2) `1 <= q `1 by A212, A252, A254;
A257: q = |[(q `1 ),(q `2 )]| by EUCLID:57;
A258: LSeg g,m1 = LSeg (G * j1,i2),q by A245, A248, A251, A253, TOPREAL1:def 5;
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 ) } ;
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 A209, A255, A256, A257, A258, TOPREAL3:16;
then ( p1 in LSeg g,m1 & LSeg g,m1 in { (LSeg g,i) where i is Element of NAT : ( 1 <= i & i + 1 <= len g ) } ) by A240, A245, A249, A251, A253, A256;
hence x in L~ g by A240, TARSKI:def 4; :: thesis:

end;

suppose ma <> len g ; :: thesis:

then ma < len g by A244, XXREAL_0:1;
then A259: ( 1 <= ma & ma + 1 <= len g & len g1 <= ma + 1 ) by A13, A14, A23, A244, NAT_1:13;
reconsider qa = g /. ma, qa1 = g /. (ma + 1) as Point of (TOP-REAL 2) ;
A260: p1 `1 <= qa `1 by A244;

A261: now

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

end;

then A262: ( qa1 `1 < qa `1 & qa1 `1 <= p1 `1 & p1 `1 <= qa `1 & qa `2 = (G * i1,i2) `2 & qa1 `2 = (G * i1,i2) `2 ) by A212, A244, A259, A260, XXREAL_0: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 ) } ;
A263: ( qa = |[(qa `1 ),(qa `2 )]| & qa1 = |[(qa1 `1 ),(qa1 `2 )]| ) by EUCLID:57;
LSeg g,ma = LSeg qa1,qa by A259, TOPREAL1:def 5
.= { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `2 = (G * i1,i2) `2 & qa1 `1 <= p2 `1 & p2 `1 <= qa `1 ) } by A262, A263, TOPREAL3:16 ;
then ( x in LSeg g,ma & LSeg g,ma in { (LSeg g,i) where i is Element of NAT : ( 1 <= i & i + 1 <= len g ) } ) by A240, A259, A260, A261;
hence x in L~ g by TARSKI:def 4; :: thesis:

end;

hence x in L~ g ; :: thesis:

end;

hence x in L~ g ; :: thesis:

end;

1 <= len g1 by A13, A14, A23, XXREAL_0:2;
then 1 in dom g1 by A30, FINSEQ_1:3;
hence g /. 1 = (f | k) /. 1 by A23, FINSEQ_4:83
.= f /. 1 by A14, FINSEQ_4:86 ;
:: thesis:
j1 + 1 <= i1 by A193, NAT_1:13;
then A264: 1 <= l by XREAL_1:21;
then A265: ( l in dom g2 & len g = (len g1) + (len g2) & len g2 = l ) by A198, FINSEQ_1:3, FINSEQ_1:35, FINSEQ_1:def 3;
reconsider m1 = i1 - l as Element of NAT ;
thus g /. (len g) = g2 /. l by A265, FINSEQ_4:84
.= G * m1,i2 by A197, A198, A265
.= f /. (len f) by A5, A26, A192 ; :: thesis:
thus len f <= len g by A5, A14, A23, A264, A265, XREAL_1:9; :: thesis:

end;

case i1 = j1 ; :: thesis:

hence contradiction by A8, A14, A24, A25, A26, A192; :: thesis:

end;

case A266: i1 < j1 ; :: thesis:

then reconsider l = j1 - i1 as Element of NAT by INT_1:18;
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
A267: ( len g2 = l & ( for n being Nat st n in dom g2 holds
g2 /. n = H₁(n) ) ) from FINSEQ_4:sch 2();
A268: dom g2 = Seg l by A267, FINSEQ_1:def 3;
take g = g1 ^ g2; :: thesis:

A269: now

let n be Element of NAT ; :: thesis:
assume n in Seg l ; :: thesis:
then A270: ( 1 <= n & n <= l ) by FINSEQ_1:3;
then ( n <= n + i1 & i1 + n <= l + i1 ) by NAT_1:11, XREAL_1:9;
then ( n <= i1 + n & i1 + n <= j1 & j1 <= len G ) by A28, FINSEQ_3:27;
then ( 1 <= i1 + n & i1 + n <= len G ) by A270, XXREAL_0:2;
hence i1 + n in dom G by FINSEQ_3:27; :: thesis:
hence [(i1 + n),i2] in Indices G by A27, A28, ZFMISC_1:106; :: thesis:

end;

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

now

let n be Element of NAT ; :: thesis:
assume A272: n in dom g2 ; :: thesis:
take m = i1 + n; :: thesis:
take k = i2; :: thesis:
thus ( [m,k] in Indices G & g2 /. n = G * m,k ) by A267, A269, A271, A272; :: thesis:

end;

then A273: for n being Element of NAT st n in dom g holds
ex i, j being Element of NAT st
( [i,j] in Indices G & g /. n = G * i,j ) by A29, GOBOARD1:39;

A274: now

let n be Element of NAT ; :: thesis:
assume ( n in dom g2 & n + 1 in dom g2 ) ; :: thesis:
then A275: ( g2 /. n = G * (i1 + n),i2 & [(i1 + n),i2] in Indices G & g2 /. (n + 1) = G * (i1 + (n + 1)),i2 & [(i1 + (n + 1)),i2] in Indices G ) by A267, A269, A271;
let l1, l2, l3, l4 be Element of NAT ; :: thesis:
assume ( [l1,l2] in Indices G & [l3,l4] in Indices G & g2 /. n = G * l1,l2 & g2 /. (n + 1) = G * l3,l4 ) ; :: thesis:
then ( l1 = i1 + n & l2 = i2 & l3 = i1 + (n + 1) & l4 = i2 & 0 <= 1 ) by A275, GOBOARD1:21;
hence (abs (l1 - l3)) + (abs (l2 - l4)) = (abs ((i1 + n) - (i1 + (n + 1)))) + 0 by ABSVALUE:7
.= abs (- 1)
.= abs 1 by COMPLEX1:138
.= 1 by ABSVALUE:def 1 ;
:: thesis:

end;

now

let l1, l2, l3, l4 be Element of NAT ; :: thesis:
assume A276: ( [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 ) ; :: thesis:
then ( g2 /. 1 = G * (i1 + 1),i2 & [(i1 + 1),i2] in Indices G & (f | k) /. (len (f | k)) = f /. k ) by A14, A267, A269, A271, FINSEQ_4:86;
then ( l1 = i1 & l2 = i2 & l3 = i1 + 1 & l4 = i2 & 0 <= 1 ) by A23, A24, A276, GOBOARD1:21;
hence (abs (l1 - l3)) + (abs (l2 - l4)) = (abs (i1 - (i1 + 1))) + 0 by ABSVALUE:7
.= abs ((i1 - i1) + (- 1))
.= abs 1 by COMPLEX1:138
.= 1 by ABSVALUE:def 1 ;
:: thesis:

end;

then for n being Element of NAT st n in dom g & n + 1 in dom g holds
for m, k, i, j being Element of NAT st [m,k] in Indices G & [i,j] in Indices G & g /. n = G * m,k & g /. (n + 1) = G * i,j holds
(abs (m - i)) + (abs (k - j)) = 1 by A29, A274, GOBOARD1:40;
hence g is_sequence_on G by A273, GOBOARD1:def 11; :: thesis:
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 ) } ;
( c1 /. i1 = c1 . i1 & c1 /. j1 = c1 . j1 ) by A28, A42, PARTFUN1:def 8;
then A277: ( c1 /. i1 = G * i1,i2 & c1 /. j1 = G * j1,i2 ) by A28, MATRIX_1:def 9;
then A278: ( (Y_axis c1) . i1 = (G * i1,i2) `2 & (Y_axis c1) . j1 = (G * j1,i2) `2 & (X_axis c1) . i1 = (G * i1,i2) `1 & (X_axis c1) . j1 = (G * j1,i2) `1 ) by A28, A42, A43, GOBOARD1:def 3, GOBOARD1:def 4;
then A279: ( (G * i1,i2) `1 < (G * j1,i2) `1 & (G * i1,i2) `2 = (G * j1,i2) `2 & G * i1,i2 = |[((G * i1,i2) `1 ),((G * i1,i2) `2 )]| & G * j1,i2 = |[((G * j1,i2) `1 ),((G * j1,i2) `2 )]| ) by A28, A33, A34, A42, A43, A266, EUCLID:57, GOBOARD1:def 2, SEQM_3:def 1;
A280: LSeg f,k = LSeg (G * i1,i2),(G * j1,i2) by A13, A24, A26, A192, TOPREAL1:def 5
.= { 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 A279, TOPREAL3:16 ;
thus L~ g = L~ f :: thesis:

proof

set lg = { (LSeg g,i) where i is Element of NAT : ( 1 <= i & i + 1 <= len g ) } ;
set lf = { (LSeg f,j) where j is Element of NAT : ( 1 <= j & j + 1 <= len f ) } ;
A281: len g = (len g1) + (len g2) by FINSEQ_1:35;

A282: now

let j be Element of NAT ; :: thesis:
assume A283: ( len g1 <= j & j <= len g ) ; :: thesis:
then reconsider w = j - (len g1) as Element of NAT by INT_1:18;
let p be Point of (TOP-REAL 2); :: thesis:
assume A284: p = g /. j ; :: thesis:
set u = i1 + w;

now

per cases ;

suppose A285: j = len g1 ; :: thesis:

1 <= len g1 by A13, A14, A23, XXREAL_0:2;
then len g1 in dom g1 by FINSEQ_3:27;
then A286: g /. (len g1) = (f | k) /. (len (f | k)) by A23, FINSEQ_4:83
.= G * i1,i2 by A14, A24, FINSEQ_4:86 ;
hence p `2 = (G * i1,i2) `2 by A284, A285; :: thesis:
thus ( (G * i1,i2) `1 <= p `1 & p `1 <= (G * j1,i2) `1 ) by A28, A33, A42, A43, A266, A278, A284, A285, A286, SEQM_3:def 1; :: thesis:
thus p in rng c1 by A28, A42, A277, A284, A285, A286, PARTFUN2:4; :: thesis:

end;

suppose A287: j <> len g1 ; :: thesis:

then A288: len g1 < j by A283, XXREAL_0:1;
A289: j - (len g1) <> 0 by A287;
then A290: w >= 1 by NAT_1:14;
A291: w + (len g1) = j ;
then A292: w <= len g2 by A281, A283, XREAL_1:8;
then A293: ( (len g1) + 1 <= j & g /. j = g2 /. w ) by A288, A290, A291, Th5, NAT_1:13;
w in dom g2 by A290, A292, FINSEQ_3:27;
then A294: ( g2 /. w = G * (i1 + w),i2 & i1 + w in dom G ) by A267, A268, A269;
then c1 /. (i1 + w) = c1 . (i1 + w) by A42, PARTFUN1:def 8;
then A295: c1 /. (i1 + w) = G * (i1 + w),i2 by A294, MATRIX_1:def 9;
then A296: ( (X_axis c1) . i1 = (G * i1,i2) `1 & (X_axis c1) . (i1 + w) = (G * (i1 + w),i2) `1 & (X_axis c1) . j1 = (G * j1,i2) `1 & (Y_axis c1) . i1 = (G * i1,i2) `2 & (Y_axis c1) . (i1 + w) = (G * (i1 + w),i2) `2 & (Y_axis c1) . j1 = (G * j1,i2) `2 ) by A28, A42, A43, A277, A294, GOBOARD1:def 3, GOBOARD1:def 4;
hence p `2 = (G * i1,i2) `2 by A28, A34, A42, A43, A284, A293, A294, GOBOARD1:def 2; :: thesis:
0 + 1 <= w by A289, NAT_1:14;
then i1 < i1 + w by XREAL_1:31;
hence (G * i1,i2) `1 <= p `1 by A28, A33, A42, A43, A284, A293, A294, A296, SEQM_3:def 1; :: thesis:

now

per cases ;

suppose i1 + w = j1 ; :: thesis:

hence p `1 <= (G * j1,i2) `1 by A284, A290, A291, A292, A294, Th5; :: thesis:

end;

suppose A297: i1 + w <> j1 ; :: thesis:

i1 + w <= i1 + l by A267, A292, XREAL_1:9;
then i1 + w < j1 by A297, XXREAL_0:1;
hence p `1 <= (G * j1,i2) `1 by A28, A33, A42, A43, A284, A293, A294, A296, SEQM_3:def 1; :: thesis:

end;

hence p `1 <= (G * j1,i2) `1 ; :: thesis:
thus p in rng c1 by A42, A284, A293, A294, A295, PARTFUN2:4; :: thesis:

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:

end;

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

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in L~ g ; :: thesis:
then consider X being set such that
A298: ( x in X & X in { (LSeg g,i) where i is Element of NAT : ( 1 <= i & i + 1 <= len g ) } ) by TARSKI:def 4;
consider i being Element of NAT such that
A299: ( X = LSeg g,i & 1 <= i & i + 1 <= len g ) by A298;

now

per cases ;

suppose A300: i + 1 <= len g1 ; :: thesis:

then ( i <= i + 1 & i + 1 <= len g1 ) by NAT_1:11;
then ( 1 <= i & i <= len g1 & 1 <= i + 1 & i + 1 <= len g1 ) by A299, XXREAL_0:2;
then ( i in dom g1 & i + 1 in dom g1 ) by FINSEQ_3:27;
then X = LSeg g1,i by A299, TOPREAL3:25;
then X in { (LSeg g1,j) where j is Element of NAT : ( 1 <= j & j + 1 <= len g1 ) } by A299, A300;
then ( x in L~ (f | k) & L~ (f | k) c= L~ f ) by A23, A298, TARSKI:def 4, TOPREAL3:27;
hence x in L~ f ; :: thesis:

end;

suppose A301: i + 1 > len g1 ; :: thesis:

then A302: ( len g1 <= i & i <= i + 1 & i + 1 <= len g ) by A299, NAT_1:13;
A303: ( 1 <= i + 1 & len g1 <= i + 1 & i <= len g ) by A299, A301, NAT_1:13;
reconsider q1 = g /. i, q2 = g /. (i + 1) as Point of (TOP-REAL 2) ;
A304: ( q1 `2 = (G * i1,i2) `2 & (G * i1,i2) `1 <= q1 `1 & q1 `1 <= (G * j1,i2) `1 & q2 `2 = (G * i1,i2) `2 & (G * i1,i2) `1 <= q2 `1 & q2 `1 <= (G * j1,i2) `1 ) by A282, A302, A303;
then A305: ( q1 = |[(q1 `1 ),(q1 `2 )]| & q2 = |[(q2 `1 ),(q1 `2 )]| ) by EUCLID:57;
A306: LSeg g,i = LSeg q2,q1 by A299, TOPREAL1:def 5;

now

per cases by XXREAL_0:1;

suppose q1 `1 > q2 `1 ; :: thesis:

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 A305, A306, TOPREAL3:16;
then consider p2 being Point of (TOP-REAL 2) such that
A307: ( p2 = x & p2 `2 = q1 `2 & q2 `1 <= p2 `1 & p2 `1 <= q1 `1 ) by A298, A299;
( (G * i1,i2) `1 <= p2 `1 & p2 `1 <= (G * j1,i2) `1 ) by A304, A307, XXREAL_0:2;
then ( x in LSeg f,k & LSeg f,k in { (LSeg f,j) where j is Element of NAT : ( 1 <= j & j + 1 <= len f ) } ) by A13, A280, A304, A307;
hence x in L~ f by TARSKI:def 4; :: thesis:

end;

suppose q1 `1 = q2 `1 ; :: thesis:

then LSeg g,i = {q1} by A305, A306, RLTOPSP1:71;
then x = q1 by A298, A299, TARSKI:def 1;
then ( x in LSeg f,k & LSeg f,k in { (LSeg f,j) where j is Element of NAT : ( 1 <= j & j + 1 <= len f ) } ) by A13, A280, A304;
hence x in L~ f by TARSKI:def 4; :: thesis:

end;

suppose q1 `1 < q2 `1 ; :: thesis:

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 A305, A306, TOPREAL3:16;
then consider p2 being Point of (TOP-REAL 2) such that
A308: ( p2 = x & p2 `2 = q1 `2 & q1 `1 <= p2 `1 & p2 `1 <= q2 `1 ) by A298, A299;
( (G * i1,i2) `1 <= p2 `1 & p2 `1 <= (G * j1,i2) `1 ) by A304, A308, XXREAL_0:2;
then ( x in LSeg f,k & LSeg f,k in { (LSeg f,j) where j is Element of NAT : ( 1 <= j & j + 1 <= len f ) } ) by A13, A280, A304, A308;
hence x in L~ f by TARSKI:def 4; :: thesis:

end;

hence x in L~ f ; :: thesis:

end;

hence x in L~ f ; :: thesis:

end;

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in L~ f ; :: thesis:
then A309: x in (L~ (f | k)) \/ (LSeg f,k) by A5, A11, Th8;

now

per cases by A309, XBOOLE_0:def 3;

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

then ( x in L~ g1 & L~ g1 c= L~ g ) by A23, Th11;
hence x in L~ g ; :: thesis:

end;

suppose x in LSeg f,k ; :: thesis:

then consider p1 being Point of (TOP-REAL 2) such that
A310: ( p1 = x & p1 `2 = (G * i1,i2) `2 & (G * i1,i2) `1 <= p1 `1 & p1 `1 <= (G * j1,i2) `1 ) by A280;
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 ) );

A311: now

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

proof

thus ( len g1 <= n & n <= len g ) by A281, XREAL_1:33; :: thesis:
let q be Point of (TOP-REAL 2); :: thesis:
assume A312: q = g /. n ; :: thesis:
1 <= len g1 by A13, A14, A23, XXREAL_0:2;
then len g1 in dom g1 by FINSEQ_3:27;
then q = (f | k) /. (len (f | k)) by A23, A312, FINSEQ_4:83
.= G * i1,i2 by A14, A24, FINSEQ_4:86 ;
hence q `1 <= p1 `1 by A310; :: thesis:

end;

A313: for n being Nat st S₃[n] holds
n <= len g ;
consider ma being Nat such that
A314: ( S₃[ma] & ( for n being Nat st S₃[n] holds
n <= ma ) ) from NAT_1:sch 6(A313, A311);
reconsider ma = ma as Element of NAT by ORDINAL1:def 13;

now

per cases ;

suppose A315: ma = len g ; :: thesis:

i1 + 1 <= j1 by A266, NAT_1:13;
then A316: 1 <= l by XREAL_1:21;
then A317: ( l in dom g2 & i1 + l = j1 ) by A267, FINSEQ_3:27;
then A318: g /. ma = g2 /. l by A267, A281, A315, FINSEQ_4:84
.= G * j1,i2 by A267, A317 ;
then (G * j1,i2) `1 <= p1 `1 by A314;
then A319: ( p1 `1 = (G * j1,i2) `1 & p1 = |[(p1 `1 ),(p1 `2 )]| ) by A310, EUCLID:57, XXREAL_0:1;
A320: ( ma <= (len g) + 1 & (len g1) + 1 <= ma & ma <= len g ) by A267, A281, A315, A316, NAT_1:11, XREAL_1:9;
0 + 1 <= ma by A267, A281, A315, A316, XREAL_1:9;
then reconsider m1 = ma - 1 as Element of NAT by INT_1:18;
A321: m1 + 1 = ma ;
then A322: m1 >= len g1 by A320, XREAL_1:8;
1 <= len g1 by A13, A14, A23, XXREAL_0:2;
then A323: 1 <= m1 by A322, XXREAL_0:2;
A324: m1 <= len g by A315, A321, NAT_1:11;
reconsider q = g /. m1 as Point of (TOP-REAL 2) ;
A325: q `2 = (G * i1,i2) `2 by A282, A322, A324;
A326: q `1 <= (G * j1,i2) `1 by A282, A322, A324;
A327: q = |[(q `1 ),(q `2 )]| by EUCLID:57;
A328: LSeg g,m1 = LSeg (G * j1,i2),q by A315, A318, A321, A323, TOPREAL1:def 5;
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 ) } ;
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 A279, A325, A326, A327, A328, TOPREAL3:16;
then ( p1 in LSeg g,m1 & LSeg g,m1 in { (LSeg g,i) where i is Element of NAT : ( 1 <= i & i + 1 <= len g ) } ) by A310, A315, A319, A321, A323, A326;
hence x in L~ g by A310, TARSKI:def 4; :: thesis:

end;

suppose ma <> len g ; :: thesis:

then ma < len g by A314, XXREAL_0:1;
then A329: ( 1 <= ma & ma + 1 <= len g & len g1 <= ma + 1 ) by A13, A14, A23, A314, NAT_1:13;
reconsider qa = g /. ma, qa1 = g /. (ma + 1) as Point of (TOP-REAL 2) ;
A330: qa `1 <= p1 `1 by A314;

A331: now

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

end;

then A332: ( qa `1 < qa1 `1 & qa `1 <= p1 `1 & p1 `1 <= qa1 `1 & qa `2 = (G * i1,i2) `2 & qa1 `2 = (G * i1,i2) `2 ) by A282, A314, A329, A330, XXREAL_0: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 ) } ;
A333: ( qa = |[(qa `1 ),(qa `2 )]| & qa1 = |[(qa1 `1 ),(qa1 `2 )]| ) by EUCLID:57;
LSeg g,ma = LSeg qa,qa1 by A329, TOPREAL1:def 5
.= { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `2 = (G * i1,i2) `2 & qa `1 <= p2 `1 & p2 `1 <= qa1 `1 ) } by A332, A333, TOPREAL3:16 ;
then ( x in LSeg g,ma & LSeg g,ma in { (LSeg g,i) where i is Element of NAT : ( 1 <= i & i + 1 <= len g ) } ) by A310, A329, A330, A331;
hence x in L~ g by TARSKI:def 4; :: thesis:

end;

hence x in L~ g ; :: thesis:

end;

hence x in L~ g ; :: thesis:

end;

1 <= len g1 by A13, A14, A23, XXREAL_0:2;
then 1 in dom g1 by FINSEQ_3:27;
hence g /. 1 = (f | k) /. 1 by A23, FINSEQ_4:83
.= f /. 1 by A14, FINSEQ_4:86 ;
:: thesis:
i1 + 1 <= j1 by A266, NAT_1:13;
then A334: 1 <= l by XREAL_1:21;
then A335: ( l in dom g2 & len g = (len g1) + l ) by A267, A271, FINSEQ_1:3, FINSEQ_1:35;
hence g /. (len g) = g2 /. l by FINSEQ_4:84
.= G * (i1 + l),i2 by A267, A335
.= f /. (len f) by A5, A26, A192 ;
:: thesis:
thus len f <= len g by A5, A14, A23, A334, A335, XREAL_1:9; :: thesis:

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:

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:

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:

end;

for n being Element of NAT holds S₂[n] from NAT_1:sch 1(A1, A3);
hence ( ( for n being Element of NAT st n in dom f holds
ex i, j being Element of NAT st
( [i,j] in Indices G & f /. n = G * i,j ) ) & f is special & ( for n being Element of 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: