let G be Go-board; :: thesis: for f being FinSequence of (TOP-REAL 2) st f is_sequence_on G & (rng f) /\ (rng (Col (G,1))) <> {} & (rng f) /\ (rng (Col (G,(width G)))) <> {} holds

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

( rng g c= rng f & g /. 1 in rng (Col (G,1)) & g /. (len g) in rng (Col (G,(width G))) & 1 <= len g & g is_sequence_on G )

let f be FinSequence of (TOP-REAL 2); :: thesis: ( f is_sequence_on G & (rng f) /\ (rng (Col (G,1))) <> {} & (rng f) /\ (rng (Col (G,(width G)))) <> {} implies ex g being FinSequence of (TOP-REAL 2) st

( rng g c= rng f & g /. 1 in rng (Col (G,1)) & g /. (len g) in rng (Col (G,(width G))) & 1 <= len g & g is_sequence_on G ) )

assume that

A1: f is_sequence_on G and

A2: (rng f) /\ (rng (Col (G,1))) <> {} and

A3: (rng f) /\ (rng (Col (G,(width G)))) <> {} ; :: thesis: ex g being FinSequence of (TOP-REAL 2) st

( rng g c= rng f & g /. 1 in rng (Col (G,1)) & g /. (len g) in rng (Col (G,(width G))) & 1 <= len g & g is_sequence_on G )

set y = the Element of (rng f) /\ (rng (Col (G,(width G))));

set x = the Element of (rng f) /\ (rng (Col (G,1)));

A4: ( the Element of (rng f) /\ (rng (Col (G,1))) in rng (Col (G,1)) & the Element of (rng f) /\ (rng (Col (G,(width G)))) in rng (Col (G,(width G))) ) by A2, A3, XBOOLE_0:def 4;

the Element of (rng f) /\ (rng (Col (G,(width G)))) in rng f by A3, XBOOLE_0:def 4;

then consider m being Element of NAT such that

A5: m in dom f and

A6: the Element of (rng f) /\ (rng (Col (G,(width G)))) = f /. m by PARTFUN2:2;

A7: 1 <= m by A5, FINSEQ_3:25;

A8: the Element of (rng f) /\ (rng (Col (G,1))) in rng f by A2, XBOOLE_0:def 4;

then consider n being Element of NAT such that

A9: n in dom f and

A10: the Element of (rng f) /\ (rng (Col (G,1))) = f /. n by PARTFUN2:2;

reconsider x = the Element of (rng f) /\ (rng (Col (G,1))) as Point of (TOP-REAL 2) by A10;

A11: 1 <= n by A9, FINSEQ_3:25;

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

( rng g c= rng f & g /. 1 in rng (Col (G,1)) & g /. (len g) in rng (Col (G,(width G))) & 1 <= len g & g is_sequence_on G )

let f be FinSequence of (TOP-REAL 2); :: thesis: ( f is_sequence_on G & (rng f) /\ (rng (Col (G,1))) <> {} & (rng f) /\ (rng (Col (G,(width G)))) <> {} implies ex g being FinSequence of (TOP-REAL 2) st

( rng g c= rng f & g /. 1 in rng (Col (G,1)) & g /. (len g) in rng (Col (G,(width G))) & 1 <= len g & g is_sequence_on G ) )

assume that

A1: f is_sequence_on G and

A2: (rng f) /\ (rng (Col (G,1))) <> {} and

A3: (rng f) /\ (rng (Col (G,(width G)))) <> {} ; :: thesis: ex g being FinSequence of (TOP-REAL 2) st

( rng g c= rng f & g /. 1 in rng (Col (G,1)) & g /. (len g) in rng (Col (G,(width G))) & 1 <= len g & g is_sequence_on G )

set y = the Element of (rng f) /\ (rng (Col (G,(width G))));

set x = the Element of (rng f) /\ (rng (Col (G,1)));

A4: ( the Element of (rng f) /\ (rng (Col (G,1))) in rng (Col (G,1)) & the Element of (rng f) /\ (rng (Col (G,(width G)))) in rng (Col (G,(width G))) ) by A2, A3, XBOOLE_0:def 4;

the Element of (rng f) /\ (rng (Col (G,(width G)))) in rng f by A3, XBOOLE_0:def 4;

then consider m being Element of NAT such that

A5: m in dom f and

A6: the Element of (rng f) /\ (rng (Col (G,(width G)))) = f /. m by PARTFUN2:2;

A7: 1 <= m by A5, FINSEQ_3:25;

A8: the Element of (rng f) /\ (rng (Col (G,1))) in rng f by A2, XBOOLE_0:def 4;

then consider n being Element of NAT such that

A9: n in dom f and

A10: the Element of (rng f) /\ (rng (Col (G,1))) = f /. n by PARTFUN2:2;

reconsider x = the Element of (rng f) /\ (rng (Col (G,1))) as Point of (TOP-REAL 2) by A10;

A11: 1 <= n by A9, FINSEQ_3:25;

per cases
( n = m or n > m or n < m )
by XXREAL_0:1;

end;

suppose A12:
n = m
; :: thesis: ex g being FinSequence of (TOP-REAL 2) st

( rng g c= rng f & g /. 1 in rng (Col (G,1)) & g /. (len g) in rng (Col (G,(width G))) & 1 <= len g & g is_sequence_on G )

( rng g c= rng f & g /. 1 in rng (Col (G,1)) & g /. (len g) in rng (Col (G,(width G))) & 1 <= len g & g is_sequence_on G )

reconsider h = <*x*> as FinSequence of (TOP-REAL 2) ;

A13: len h = 1 by FINSEQ_1:39;

take h ; :: thesis: ( rng h c= rng f & h /. 1 in rng (Col (G,1)) & h /. (len h) in rng (Col (G,(width G))) & 1 <= len h & h is_sequence_on G )

thus rng h c= rng f by A17; :: thesis: ( h /. 1 in rng (Col (G,1)) & h /. (len h) in rng (Col (G,(width G))) & 1 <= len h & h is_sequence_on G )

1 in Seg 1 by FINSEQ_1:1;

hence ( h /. 1 in rng (Col (G,1)) & h /. (len h) in rng (Col (G,(width G))) ) by A10, A4, A6, A12, A13, A14; :: thesis: ( 1 <= len h & h is_sequence_on G )

A20: dom h = Seg (len h) by FINSEQ_1:def 3;

end;A13: len h = 1 by FINSEQ_1:39;

A14: now :: thesis: for k being Nat st k in Seg 1 holds

h /. k = x

A17:
rng h c= rng f
h /. k = x

let k be Nat; :: thesis: ( k in Seg 1 implies h /. k = x )

assume A15: k in Seg 1 ; :: thesis: h /. k = x

then A16: k = 1 by FINSEQ_1:2, TARSKI:def 1;

k in dom h by A15, FINSEQ_1:def 8;

hence h /. k = h . k by PARTFUN1:def 6

.= x by A16, FINSEQ_1:40 ;

:: thesis: verum

end;assume A15: k in Seg 1 ; :: thesis: h /. k = x

then A16: k = 1 by FINSEQ_1:2, TARSKI:def 1;

k in dom h by A15, FINSEQ_1:def 8;

hence h /. k = h . k by PARTFUN1:def 6

.= x by A16, FINSEQ_1:40 ;

:: thesis: verum

proof

reconsider h = h as FinSequence of (TOP-REAL 2) ;
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in rng h or z in rng f )

assume z in rng h ; :: thesis: z in rng f

then consider i being Element of NAT such that

A18: i in dom h and

A19: z = h /. i by PARTFUN2:2;

i in Seg 1 by A18, FINSEQ_1:def 8;

hence z in rng f by A8, A14, A19; :: thesis: verum

end;assume z in rng h ; :: thesis: z in rng f

then consider i being Element of NAT such that

A18: i in dom h and

A19: z = h /. i by PARTFUN2:2;

i in Seg 1 by A18, FINSEQ_1:def 8;

hence z in rng f by A8, A14, A19; :: thesis: verum

take h ; :: thesis: ( rng h c= rng f & h /. 1 in rng (Col (G,1)) & h /. (len h) in rng (Col (G,(width G))) & 1 <= len h & h is_sequence_on G )

thus rng h c= rng f by A17; :: thesis: ( h /. 1 in rng (Col (G,1)) & h /. (len h) in rng (Col (G,(width G))) & 1 <= len h & h is_sequence_on G )

1 in Seg 1 by FINSEQ_1:1;

hence ( h /. 1 in rng (Col (G,1)) & h /. (len h) in rng (Col (G,(width G))) ) by A10, A4, A6, A12, A13, A14; :: thesis: ( 1 <= len h & h is_sequence_on G )

A20: dom h = Seg (len h) by FINSEQ_1:def 3;

A21: now :: thesis: for i being Nat st i in dom h & i + 1 in dom h holds

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

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

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

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

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

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

assume that

A22: i in dom h and

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

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

i = 1 by A13, A20, A22, FINSEQ_1:2, TARSKI:def 1;

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

|.(i1 - j1).| + |.(i2 - j2).| = 1 by A13, A20, A23, FINSEQ_1:2, TARSKI:def 1; :: thesis: verum

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

assume that

A22: i in dom h and

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

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

i = 1 by A13, A20, A22, FINSEQ_1:2, TARSKI:def 1;

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

|.(i1 - j1).| + |.(i2 - j2).| = 1 by A13, A20, A23, FINSEQ_1:2, TARSKI:def 1; :: thesis: verum

now :: thesis: for i being Nat st i in dom h holds

ex i1, i2 being Nat st

( [i1,i2] in Indices G & h /. i = G * (i1,i2) )

hence
( 1 <= len h & h is_sequence_on G )
by A21, FINSEQ_1:39; :: thesis: verumex i1, i2 being Nat st

( [i1,i2] in Indices G & h /. i = G * (i1,i2) )

consider i1, i2 being Nat such that

A24: ( [i1,i2] in Indices G & f /. n = G * (i1,i2) ) by A1, A9;

let i be Nat; :: thesis: ( i in dom h implies ex i1, i2 being Nat st

( [i1,i2] in Indices G & h /. i = G * (i1,i2) ) )

assume A25: i in dom h ; :: thesis: ex i1, i2 being Nat st

( [i1,i2] in Indices G & h /. i = G * (i1,i2) )

take i1 = i1; :: thesis: ex i2 being Nat st

( [i1,i2] in Indices G & h /. i = G * (i1,i2) )

take i2 = i2; :: thesis: ( [i1,i2] in Indices G & h /. i = G * (i1,i2) )

thus ( [i1,i2] in Indices G & h /. i = G * (i1,i2) ) by A10, A13, A14, A20, A25, A24; :: thesis: verum

end;A24: ( [i1,i2] in Indices G & f /. n = G * (i1,i2) ) by A1, A9;

let i be Nat; :: thesis: ( i in dom h implies ex i1, i2 being Nat st

( [i1,i2] in Indices G & h /. i = G * (i1,i2) ) )

assume A25: i in dom h ; :: thesis: ex i1, i2 being Nat st

( [i1,i2] in Indices G & h /. i = G * (i1,i2) )

take i1 = i1; :: thesis: ex i2 being Nat st

( [i1,i2] in Indices G & h /. i = G * (i1,i2) )

take i2 = i2; :: thesis: ( [i1,i2] in Indices G & h /. i = G * (i1,i2) )

thus ( [i1,i2] in Indices G & h /. i = G * (i1,i2) ) by A10, A13, A14, A20, A25, A24; :: thesis: verum

suppose A26:
n > m
; :: thesis: ex g being FinSequence of (TOP-REAL 2) st

( rng g c= rng f & g /. 1 in rng (Col (G,1)) & g /. (len g) in rng (Col (G,(width G))) & 1 <= len g & g is_sequence_on G )

( rng g c= rng f & g /. 1 in rng (Col (G,1)) & g /. (len g) in rng (Col (G,(width G))) & 1 <= len g & g is_sequence_on G )

n <= n + 1
by NAT_1:11;

then reconsider l = (n + 1) - m as Element of NAT by A26, INT_1:5, XXREAL_0:2;

set f1 = f | n;

defpred S_{1}[ Nat, set ] means for k being Nat st $1 + k = n + 1 holds

$2 = (f | n) /. k;

A27: n in Seg n by A11, FINSEQ_1:1;

ex p being Point of (TOP-REAL 2) st S_{1}[i,p]

A31: ( len g = l & ( for i being Nat st i in Seg l holds

S_{1}[i,g /. i] ) )
from FINSEQ_4:sch 1(A30);

take g ; :: thesis: ( rng g c= rng f & g /. 1 in rng (Col (G,1)) & g /. (len g) in rng (Col (G,(width G))) & 1 <= len g & g is_sequence_on G )

A32: dom g = Seg (len g) by FINSEQ_1:def 3;

A33: for i being Nat st i in Seg l holds

( (n + 1) - i is Element of NAT & (f | n) /. ((n + 1) - i) = f /. ((n + 1) - i) & (n + 1) - i in dom f )

then A48: m + 1 <= n + 1 by NAT_1:13;

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

then 1 in Seg l by FINSEQ_1:1;

then g /. 1 = (f | n) /. n by A31

.= f /. n by A9, A27, FINSEQ_4:71 ;

hence g /. 1 in rng (Col (G,1)) by A2, A10, XBOOLE_0:def 4; :: thesis: ( g /. (len g) in rng (Col (G,(width G))) & 1 <= len g & g is_sequence_on G )

A50: m in Seg n by A7, A26, FINSEQ_1:1;

reconsider ww = (n + 1) - l as Element of NAT ;

A51: l + ww = n + 1 ;

len g in dom g by A31, A49, FINSEQ_3:25;

then g /. (len g) = (f | n) /. ww by A31, A32, A51

.= f /. m by A9, A50, FINSEQ_4:71 ;

hence g /. (len g) in rng (Col (G,(width G))) by A3, A6, XBOOLE_0:def 4; :: thesis: ( 1 <= len g & g is_sequence_on G )

end;then reconsider l = (n + 1) - m as Element of NAT by A26, INT_1:5, XXREAL_0:2;

set f1 = f | n;

defpred S

$2 = (f | n) /. k;

A27: n in Seg n by A11, FINSEQ_1:1;

A28: now :: thesis: for i being Nat st i in Seg l holds

(n + 1) - i is Element of NAT

A30:
for i being Nat st i in Seg l holds (n + 1) - i is Element of NAT

let i be Nat; :: thesis: ( i in Seg l implies (n + 1) - i is Element of NAT )

assume i in Seg l ; :: thesis: (n + 1) - i is Element of NAT

then A29: i <= l by FINSEQ_1:1;

l <= (n + 1) - 0 by XREAL_1:13;

hence (n + 1) - i is Element of NAT by A29, INT_1:5, XXREAL_0:2; :: thesis: verum

end;assume i in Seg l ; :: thesis: (n + 1) - i is Element of NAT

then A29: i <= l by FINSEQ_1:1;

l <= (n + 1) - 0 by XREAL_1:13;

hence (n + 1) - i is Element of NAT by A29, INT_1:5, XXREAL_0:2; :: thesis: verum

ex p being Point of (TOP-REAL 2) st S

proof

consider g being FinSequence of (TOP-REAL 2) such that
let i be Nat; :: thesis: ( i in Seg l implies ex p being Point of (TOP-REAL 2) st S_{1}[i,p] )

assume i in Seg l ; :: thesis: ex p being Point of (TOP-REAL 2) st S_{1}[i,p]

then reconsider a = (n + 1) - i as Element of NAT by A28;

take (f | n) /. a ; :: thesis: S_{1}[i,(f | n) /. a]

let k be Nat; :: thesis: ( i + k = n + 1 implies (f | n) /. a = (f | n) /. k )

assume i + k = n + 1 ; :: thesis: (f | n) /. a = (f | n) /. k

hence (f | n) /. a = (f | n) /. k ; :: thesis: verum

end;assume i in Seg l ; :: thesis: ex p being Point of (TOP-REAL 2) st S

then reconsider a = (n + 1) - i as Element of NAT by A28;

take (f | n) /. a ; :: thesis: S

let k be Nat; :: thesis: ( i + k = n + 1 implies (f | n) /. a = (f | n) /. k )

assume i + k = n + 1 ; :: thesis: (f | n) /. a = (f | n) /. k

hence (f | n) /. a = (f | n) /. k ; :: thesis: verum

A31: ( len g = l & ( for i being Nat st i in Seg l holds

S

take g ; :: thesis: ( rng g c= rng f & g /. 1 in rng (Col (G,1)) & g /. (len g) in rng (Col (G,(width G))) & 1 <= len g & g is_sequence_on G )

A32: dom g = Seg (len g) by FINSEQ_1:def 3;

A33: for i being Nat st i in Seg l holds

( (n + 1) - i is Element of NAT & (f | n) /. ((n + 1) - i) = f /. ((n + 1) - i) & (n + 1) - i in dom f )

proof

thus
rng g c= rng f
:: thesis: ( g /. 1 in rng (Col (G,1)) & g /. (len g) in rng (Col (G,(width G))) & 1 <= len g & g is_sequence_on G )
let i be Nat; :: thesis: ( i in Seg l implies ( (n + 1) - i is Element of NAT & (f | n) /. ((n + 1) - i) = f /. ((n + 1) - i) & (n + 1) - i in dom f ) )

assume A34: i in Seg l ; :: thesis: ( (n + 1) - i is Element of NAT & (f | n) /. ((n + 1) - i) = f /. ((n + 1) - i) & (n + 1) - i in dom f )

then A35: i <= l by FINSEQ_1:1;

l <= (n + 1) - 0 by XREAL_1:13;

then reconsider w = (n + 1) - i as Element of NAT by A35, INT_1:5, XXREAL_0:2;

1 <= i by A34, FINSEQ_1:1;

then A36: (n + 1) - i <= (n + 1) - 1 by XREAL_1:13;

(n + 1) - l <= (n + 1) - i by A35, XREAL_1:13;

then 1 <= (n + 1) - i by A7, XXREAL_0:2;

then w in Seg n by A36, FINSEQ_1:1;

hence ( (n + 1) - i is Element of NAT & (f | n) /. ((n + 1) - i) = f /. ((n + 1) - i) & (n + 1) - i in dom f ) by A9, FINSEQ_4:71; :: thesis: verum

end;assume A34: i in Seg l ; :: thesis: ( (n + 1) - i is Element of NAT & (f | n) /. ((n + 1) - i) = f /. ((n + 1) - i) & (n + 1) - i in dom f )

then A35: i <= l by FINSEQ_1:1;

l <= (n + 1) - 0 by XREAL_1:13;

then reconsider w = (n + 1) - i as Element of NAT by A35, INT_1:5, XXREAL_0:2;

1 <= i by A34, FINSEQ_1:1;

then A36: (n + 1) - i <= (n + 1) - 1 by XREAL_1:13;

(n + 1) - l <= (n + 1) - i by A35, XREAL_1:13;

then 1 <= (n + 1) - i by A7, XXREAL_0:2;

then w in Seg n by A36, FINSEQ_1:1;

hence ( (n + 1) - i is Element of NAT & (f | n) /. ((n + 1) - i) = f /. ((n + 1) - i) & (n + 1) - i in dom f ) by A9, FINSEQ_4:71; :: thesis: verum

proof

A40:
dom g = Seg (len g)
by FINSEQ_1:def 3;
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in rng g or z in rng f )

assume z in rng g ; :: thesis: z in rng f

then consider i being Element of NAT such that

A37: i in dom g and

A38: z = g /. i by PARTFUN2:2;

reconsider yy = (n + 1) - i as Element of NAT by A28, A31, A32, A37;

i + yy = n + 1 ;

then A39: z = (f | n) /. yy by A31, A32, A37, A38;

( (f | n) /. yy = f /. yy & yy in dom f ) by A33, A31, A32, A37;

hence z in rng f by A39, PARTFUN2:2; :: thesis: verum

end;assume z in rng g ; :: thesis: z in rng f

then consider i being Element of NAT such that

A37: i in dom g and

A38: z = g /. i by PARTFUN2:2;

reconsider yy = (n + 1) - i as Element of NAT by A28, A31, A32, A37;

i + yy = n + 1 ;

then A39: z = (f | n) /. yy by A31, A32, A37, A38;

( (f | n) /. yy = f /. yy & yy in dom f ) by A33, A31, A32, A37;

hence z in rng f by A39, PARTFUN2:2; :: thesis: verum

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

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

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

m + 1 <= n
by A26, NAT_1:13;for i1, i2, j1, j2 being Nat st [i1,i2] in Indices G & [j1,j2] in Indices G & g /. i = G * (i1,i2) & g /. (i + 1) = G * (j1,j2) holds

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

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

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

assume that

A42: i in dom g and

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

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

let i1, i2, j1, j2 be Nat; :: thesis: ( [i1,i2] in Indices G & [j1,j2] in Indices G & g /. i = G * (i1,i2) & g /. (i + 1) = G * (j1,j2) implies 1 = |.(i1 - j1).| + |.(i2 - j2).| )

assume A44: ( [i1,i2] in Indices G & [j1,j2] in Indices G & g /. i = G * (i1,i2) & g /. (i + 1) = G * (j1,j2) ) ; :: thesis: 1 = |.(i1 - j1).| + |.(i2 - j2).|

reconsider xx = (n + 1) - (i + 1) as Element of NAT by A28, A31, A40, A43;

(i + 1) + xx = n + 1 ;

then g /. (i + 1) = (f | n) /. xx by A31, A32, A43;

then A45: g /. (i + 1) = f /. xx by A33, A31, A32, A43;

A46: xx + 1 = (n + 1) - i ;

reconsider ww = (n + 1) - i as Element of NAT by A28, A31, A40, A42;

i + ww = n + 1 ;

then g /. i = (f | n) /. ww by A31, A32, A42;

then A47: g /. i = f /. ww by A33, A31, A32, A42;

( ww in dom f & xx in dom f ) by A33, A31, A32, A42, A43;

hence 1 = |.(j1 - i1).| + |.(j2 - i2).| by A1, A47, A45, A46, A44

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

.= |.(i1 - j1).| + |.(- (i2 - j2)).| by COMPLEX1:52

.= |.(i1 - j1).| + |.(i2 - j2).| by COMPLEX1:52 ;

:: thesis: verum

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

assume that

A42: i in dom g and

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

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

let i1, i2, j1, j2 be Nat; :: thesis: ( [i1,i2] in Indices G & [j1,j2] in Indices G & g /. i = G * (i1,i2) & g /. (i + 1) = G * (j1,j2) implies 1 = |.(i1 - j1).| + |.(i2 - j2).| )

assume A44: ( [i1,i2] in Indices G & [j1,j2] in Indices G & g /. i = G * (i1,i2) & g /. (i + 1) = G * (j1,j2) ) ; :: thesis: 1 = |.(i1 - j1).| + |.(i2 - j2).|

reconsider xx = (n + 1) - (i + 1) as Element of NAT by A28, A31, A40, A43;

(i + 1) + xx = n + 1 ;

then g /. (i + 1) = (f | n) /. xx by A31, A32, A43;

then A45: g /. (i + 1) = f /. xx by A33, A31, A32, A43;

A46: xx + 1 = (n + 1) - i ;

reconsider ww = (n + 1) - i as Element of NAT by A28, A31, A40, A42;

i + ww = n + 1 ;

then g /. i = (f | n) /. ww by A31, A32, A42;

then A47: g /. i = f /. ww by A33, A31, A32, A42;

( ww in dom f & xx in dom f ) by A33, A31, A32, A42, A43;

hence 1 = |.(j1 - i1).| + |.(j2 - i2).| by A1, A47, A45, A46, A44

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

.= |.(i1 - j1).| + |.(- (i2 - j2)).| by COMPLEX1:52

.= |.(i1 - j1).| + |.(i2 - j2).| by COMPLEX1:52 ;

:: thesis: verum

then A48: m + 1 <= n + 1 by NAT_1:13;

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

then 1 in Seg l by FINSEQ_1:1;

then g /. 1 = (f | n) /. n by A31

.= f /. n by A9, A27, FINSEQ_4:71 ;

hence g /. 1 in rng (Col (G,1)) by A2, A10, XBOOLE_0:def 4; :: thesis: ( g /. (len g) in rng (Col (G,(width G))) & 1 <= len g & g is_sequence_on G )

A50: m in Seg n by A7, A26, FINSEQ_1:1;

reconsider ww = (n + 1) - l as Element of NAT ;

A51: l + ww = n + 1 ;

len g in dom g by A31, A49, FINSEQ_3:25;

then g /. (len g) = (f | n) /. ww by A31, A32, A51

.= f /. m by A9, A50, FINSEQ_4:71 ;

hence g /. (len g) in rng (Col (G,(width G))) by A3, A6, XBOOLE_0:def 4; :: thesis: ( 1 <= len g & g is_sequence_on G )

now :: thesis: for i being Nat st i in dom g holds

ex i1, i2 being Nat st

( [i1,i2] in Indices G & g /. i = G * (i1,i2) )

hence
( 1 <= len g & g is_sequence_on G )
by A31, A48, A41, XREAL_1:19; :: thesis: verumex i1, i2 being Nat st

( [i1,i2] in Indices G & g /. i = G * (i1,i2) )

let i be Nat; :: thesis: ( i in dom g implies ex i1, i2 being Nat st

( [i1,i2] in Indices G & g /. i = G * (i1,i2) ) )

assume A52: i in dom g ; :: thesis: ex i1, i2 being Nat st

( [i1,i2] in Indices G & g /. i = G * (i1,i2) )

then reconsider ww = (n + 1) - i as Element of NAT by A28, A31, A40;

ww in dom f by A33, A31, A32, A52;

then consider i1, i2 being Nat such that

A53: ( [i1,i2] in Indices G & f /. ww = G * (i1,i2) ) by A1;

take i1 = i1; :: thesis: ex i2 being Nat st

( [i1,i2] in Indices G & g /. i = G * (i1,i2) )

take i2 = i2; :: thesis: ( [i1,i2] in Indices G & g /. i = G * (i1,i2) )

i + ww = n + 1 ;

then g /. i = (f | n) /. ww by A31, A32, A52;

hence ( [i1,i2] in Indices G & g /. i = G * (i1,i2) ) by A33, A31, A32, A52, A53; :: thesis: verum

end;( [i1,i2] in Indices G & g /. i = G * (i1,i2) ) )

assume A52: i in dom g ; :: thesis: ex i1, i2 being Nat st

( [i1,i2] in Indices G & g /. i = G * (i1,i2) )

then reconsider ww = (n + 1) - i as Element of NAT by A28, A31, A40;

ww in dom f by A33, A31, A32, A52;

then consider i1, i2 being Nat such that

A53: ( [i1,i2] in Indices G & f /. ww = G * (i1,i2) ) by A1;

take i1 = i1; :: thesis: ex i2 being Nat st

( [i1,i2] in Indices G & g /. i = G * (i1,i2) )

take i2 = i2; :: thesis: ( [i1,i2] in Indices G & g /. i = G * (i1,i2) )

i + ww = n + 1 ;

then g /. i = (f | n) /. ww by A31, A32, A52;

hence ( [i1,i2] in Indices G & g /. i = G * (i1,i2) ) by A33, A31, A32, A52, A53; :: thesis: verum

suppose A54:
n < m
; :: thesis: ex g being FinSequence of (TOP-REAL 2) st

( rng g c= rng f & g /. 1 in rng (Col (G,1)) & g /. (len g) in rng (Col (G,(width G))) & 1 <= len g & g is_sequence_on G )

( rng g c= rng f & g /. 1 in rng (Col (G,1)) & g /. (len g) in rng (Col (G,(width G))) & 1 <= len g & g is_sequence_on G )

then A55:
n in Seg m
by A11, FINSEQ_1:1;

m <= m + 1 by NAT_1:11;

then reconsider l = (m + 1) - n as Element of NAT by A54, INT_1:5, XXREAL_0:2;

reconsider w = n - 1 as Element of NAT by A11, INT_1:5;

set f1 = f | m;

defpred S_{1}[ Nat, set ] means $2 = (f | m) /. (w + $1);

A56: for i being Nat st i in Seg l holds

ex p being Point of (TOP-REAL 2) st S_{1}[i,p]
;

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

A57: ( len g = l & ( for i being Nat st i in Seg l holds

S_{1}[i,g /. i] ) )
from FINSEQ_4:sch 1(A56);

reconsider ww = (m + 1) - n as Element of NAT by A57;

A58: m in Seg m by A7, FINSEQ_1:1;

take g ; :: thesis: ( rng g c= rng f & g /. 1 in rng (Col (G,1)) & g /. (len g) in rng (Col (G,(width G))) & 1 <= len g & g is_sequence_on G )

A59: dom g = Seg l by A57, FINSEQ_1:def 3;

A60: for i being Nat st i in Seg l holds

( n - 1 is Element of NAT & (f | m) /. (w + i) = f /. (w + i) & (n - 1) + i in dom f )

thus rng g c= rng f :: thesis: ( g /. 1 in rng (Col (G,1)) & g /. (len g) in rng (Col (G,(width G))) & 1 <= len g & g is_sequence_on G )

then A73: n + 1 <= m + 1 by NAT_1:13;

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

then 1 in Seg l by FINSEQ_1:1;

then g /. 1 = (f | m) /. ((n - 1) + 1) by A57

.= f /. n by A5, A55, FINSEQ_4:71 ;

hence g /. 1 in rng (Col (G,1)) by A2, A10, XBOOLE_0:def 4; :: thesis: ( g /. (len g) in rng (Col (G,(width G))) & 1 <= len g & g is_sequence_on G )

len g in dom g by A57, A74, FINSEQ_3:25;

then g /. (len g) = (f | m) /. (w + ww) by A57, A59

.= f /. m by A5, A58, FINSEQ_4:71 ;

hence g /. (len g) in rng (Col (G,(width G))) by A3, A6, XBOOLE_0:def 4; :: thesis: ( 1 <= len g & g is_sequence_on G )

end;m <= m + 1 by NAT_1:11;

then reconsider l = (m + 1) - n as Element of NAT by A54, INT_1:5, XXREAL_0:2;

reconsider w = n - 1 as Element of NAT by A11, INT_1:5;

set f1 = f | m;

defpred S

A56: for i being Nat st i in Seg l holds

ex p being Point of (TOP-REAL 2) st S

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

A57: ( len g = l & ( for i being Nat st i in Seg l holds

S

reconsider ww = (m + 1) - n as Element of NAT by A57;

A58: m in Seg m by A7, FINSEQ_1:1;

take g ; :: thesis: ( rng g c= rng f & g /. 1 in rng (Col (G,1)) & g /. (len g) in rng (Col (G,(width G))) & 1 <= len g & g is_sequence_on G )

A59: dom g = Seg l by A57, FINSEQ_1:def 3;

A60: for i being Nat st i in Seg l holds

( n - 1 is Element of NAT & (f | m) /. (w + i) = f /. (w + i) & (n - 1) + i in dom f )

proof

let i be Nat; :: thesis: ( i in Seg l implies ( n - 1 is Element of NAT & (f | m) /. (w + i) = f /. (w + i) & (n - 1) + i in dom f ) )

assume A61: i in Seg l ; :: thesis: ( n - 1 is Element of NAT & (f | m) /. (w + i) = f /. (w + i) & (n - 1) + i in dom f )

then i <= l by FINSEQ_1:1;

then i + n <= l + n by XREAL_1:7;

then A62: (i + n) - 1 <= m by XREAL_1:20;

1 <= i by A61, FINSEQ_1:1;

then 0 + 1 <= w + i by XREAL_1:7;

then w + i in Seg m by A62, FINSEQ_1:1;

hence ( n - 1 is Element of NAT & (f | m) /. (w + i) = f /. (w + i) & (n - 1) + i in dom f ) by A5, FINSEQ_4:71; :: thesis: verum

end;assume A61: i in Seg l ; :: thesis: ( n - 1 is Element of NAT & (f | m) /. (w + i) = f /. (w + i) & (n - 1) + i in dom f )

then i <= l by FINSEQ_1:1;

then i + n <= l + n by XREAL_1:7;

then A62: (i + n) - 1 <= m by XREAL_1:20;

1 <= i by A61, FINSEQ_1:1;

then 0 + 1 <= w + i by XREAL_1:7;

then w + i in Seg m by A62, FINSEQ_1:1;

hence ( n - 1 is Element of NAT & (f | m) /. (w + i) = f /. (w + i) & (n - 1) + i in dom f ) by A5, FINSEQ_4:71; :: thesis: verum

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

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

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

A69:
dom g = Seg (len g)
by FINSEQ_1:def 3;for i1, i2, j1, j2 being Nat st [i1,i2] in Indices G & [j1,j2] in Indices G & g /. i = G * (i1,i2) & g /. (i + 1) = G * (j1,j2) holds

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

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

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

assume that

A64: i in dom g and

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

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

g /. i = (f | m) /. (w + i) by A57, A59, A64;

then A66: g /. i = f /. (w + i) by A60, A59, A64;

g /. (i + 1) = (f | m) /. (w + (i + 1)) by A57, A59, A65;

then A67: ( (w + i) + 1 in dom f & g /. (i + 1) = f /. ((w + i) + 1) ) by A60, A59, A65;

let i1, i2, j1, j2 be Nat; :: thesis: ( [i1,i2] in Indices G & [j1,j2] in Indices G & g /. i = G * (i1,i2) & g /. (i + 1) = G * (j1,j2) implies |.(i1 - j1).| + |.(i2 - j2).| = 1 )

assume A68: ( [i1,i2] in Indices G & [j1,j2] in Indices G & g /. i = G * (i1,i2) & g /. (i + 1) = G * (j1,j2) ) ; :: thesis: |.(i1 - j1).| + |.(i2 - j2).| = 1

w + i in dom f by A60, A59, A64;

hence |.(i1 - j1).| + |.(i2 - j2).| = 1 by A1, A66, A67, A68; :: thesis: verum

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

assume that

A64: i in dom g and

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

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

g /. i = (f | m) /. (w + i) by A57, A59, A64;

then A66: g /. i = f /. (w + i) by A60, A59, A64;

g /. (i + 1) = (f | m) /. (w + (i + 1)) by A57, A59, A65;

then A67: ( (w + i) + 1 in dom f & g /. (i + 1) = f /. ((w + i) + 1) ) by A60, A59, A65;

let i1, i2, j1, j2 be Nat; :: thesis: ( [i1,i2] in Indices G & [j1,j2] in Indices G & g /. i = G * (i1,i2) & g /. (i + 1) = G * (j1,j2) implies |.(i1 - j1).| + |.(i2 - j2).| = 1 )

assume A68: ( [i1,i2] in Indices G & [j1,j2] in Indices G & g /. i = G * (i1,i2) & g /. (i + 1) = G * (j1,j2) ) ; :: thesis: |.(i1 - j1).| + |.(i2 - j2).| = 1

w + i in dom f by A60, A59, A64;

hence |.(i1 - j1).| + |.(i2 - j2).| = 1 by A1, A66, A67, A68; :: thesis: verum

thus rng g c= rng f :: thesis: ( g /. 1 in rng (Col (G,1)) & g /. (len g) in rng (Col (G,(width G))) & 1 <= len g & g is_sequence_on G )

proof

n + 1 <= m
by A54, NAT_1:13;
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in rng g or z in rng f )

assume z in rng g ; :: thesis: z in rng f

then consider i being Element of NAT such that

A70: i in dom g and

A71: z = g /. i by PARTFUN2:2;

A72: w + i in dom f by A60, A57, A69, A70;

( z = (f | m) /. (w + i) & (f | m) /. (w + i) = f /. (w + i) ) by A60, A57, A69, A70, A71;

hence z in rng f by A72, PARTFUN2:2; :: thesis: verum

end;assume z in rng g ; :: thesis: z in rng f

then consider i being Element of NAT such that

A70: i in dom g and

A71: z = g /. i by PARTFUN2:2;

A72: w + i in dom f by A60, A57, A69, A70;

( z = (f | m) /. (w + i) & (f | m) /. (w + i) = f /. (w + i) ) by A60, A57, A69, A70, A71;

hence z in rng f by A72, PARTFUN2:2; :: thesis: verum

then A73: n + 1 <= m + 1 by NAT_1:13;

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

then 1 in Seg l by FINSEQ_1:1;

then g /. 1 = (f | m) /. ((n - 1) + 1) by A57

.= f /. n by A5, A55, FINSEQ_4:71 ;

hence g /. 1 in rng (Col (G,1)) by A2, A10, XBOOLE_0:def 4; :: thesis: ( g /. (len g) in rng (Col (G,(width G))) & 1 <= len g & g is_sequence_on G )

len g in dom g by A57, A74, FINSEQ_3:25;

then g /. (len g) = (f | m) /. (w + ww) by A57, A59

.= f /. m by A5, A58, FINSEQ_4:71 ;

hence g /. (len g) in rng (Col (G,(width G))) by A3, A6, XBOOLE_0:def 4; :: thesis: ( 1 <= len g & g is_sequence_on G )

now :: thesis: for i being Nat st i in dom g holds

ex i1, i2 being Nat st

( [i1,i2] in Indices G & g /. i = G * (i1,i2) )

hence
( 1 <= len g & g is_sequence_on G )
by A57, A73, A63, XREAL_1:19; :: thesis: verumex i1, i2 being Nat st

( [i1,i2] in Indices G & g /. i = G * (i1,i2) )

let i be Nat; :: thesis: ( i in dom g implies ex i1, i2 being Nat st

( [i1,i2] in Indices G & g /. i = G * (i1,i2) ) )

assume A75: i in dom g ; :: thesis: ex i1, i2 being Nat st

( [i1,i2] in Indices G & g /. i = G * (i1,i2) )

then w + i in dom f by A60, A59;

then consider i1, i2 being Nat such that

A76: ( [i1,i2] in Indices G & f /. (w + i) = G * (i1,i2) ) by A1;

take i1 = i1; :: thesis: ex i2 being Nat st

( [i1,i2] in Indices G & g /. i = G * (i1,i2) )

take i2 = i2; :: thesis: ( [i1,i2] in Indices G & g /. i = G * (i1,i2) )

g /. i = (f | m) /. (w + i) by A57, A59, A75;

hence ( [i1,i2] in Indices G & g /. i = G * (i1,i2) ) by A60, A59, A75, A76; :: thesis: verum

end;( [i1,i2] in Indices G & g /. i = G * (i1,i2) ) )

assume A75: i in dom g ; :: thesis: ex i1, i2 being Nat st

( [i1,i2] in Indices G & g /. i = G * (i1,i2) )

then w + i in dom f by A60, A59;

then consider i1, i2 being Nat such that

A76: ( [i1,i2] in Indices G & f /. (w + i) = G * (i1,i2) ) by A1;

take i1 = i1; :: thesis: ex i2 being Nat st

( [i1,i2] in Indices G & g /. i = G * (i1,i2) )

take i2 = i2; :: thesis: ( [i1,i2] in Indices G & g /. i = G * (i1,i2) )

g /. i = (f | m) /. (w + i) by A57, A59, A75;

hence ( [i1,i2] in Indices G & g /. i = G * (i1,i2) ) by A60, A59, A75, A76; :: thesis: verum