let f be non empty FinSequence of (TOP-REAL 2); for G being Go-board st f is_sequence_on G & ex i being Nat st
( [1,i] in Indices G & G * (1,i) in rng f ) & ex i being Nat st
( [(len G),i] in Indices G & G * ((len G),i) in rng f ) holds
proj1 .: (rng f) = proj1 .: (Values G)
let G be Go-board; ( f is_sequence_on G & ex i being Nat st
( [1,i] in Indices G & G * (1,i) in rng f ) & ex i being Nat st
( [(len G),i] in Indices G & G * ((len G),i) in rng f ) implies proj1 .: (rng f) = proj1 .: (Values G) )
assume A1:
f is_sequence_on G
; ( for i being Nat holds
( not [1,i] in Indices G or not G * (1,i) in rng f ) or for i being Nat holds
( not [(len G),i] in Indices G or not G * ((len G),i) in rng f ) or proj1 .: (rng f) = proj1 .: (Values G) )
given i1 being Nat such that A2:
[1,i1] in Indices G
and
A3:
G * (1,i1) in rng f
; ( for i being Nat holds
( not [(len G),i] in Indices G or not G * ((len G),i) in rng f ) or proj1 .: (rng f) = proj1 .: (Values G) )
consider k1 being object such that
A4:
k1 in dom f
and
A5:
G * (1,i1) = f . k1
by A3, FUNCT_1:def 3;
reconsider k1 = k1 as Nat by A4;
A6:
1 <= k1
by A4, FINSEQ_3:25;
given i2 being Nat such that A7:
[(len G),i2] in Indices G
and
A8:
G * ((len G),i2) in rng f
; proj1 .: (rng f) = proj1 .: (Values G)
consider k2 being object such that
A9:
k2 in dom f
and
A10:
G * ((len G),i2) = f . k2
by A8, FUNCT_1:def 3;
reconsider k2 = k2 as Nat by A9;
A11:
k2 <= len f
by A9, FINSEQ_3:25;
A12:
k1 <= len f
by A4, FINSEQ_3:25;
set g = mid (f,k1,k2);
A13:
mid (f,k1,k2) is_sequence_on G
by A1, Th27;
A14:
1 <= k2
by A9, FINSEQ_3:25;
A16:
Values G = { (G * (i,j)) where i, j is Nat : [i,j] in Indices G }
by MATRIX_0:39;
A17:
proj1 .: (Values G) c= proj1 .: (rng (mid (f,k1,k2)))
proof
assume
not
proj1 .: (Values G) c= proj1 .: (rng (mid (f,k1,k2)))
;
contradiction
then consider x being
Element of
REAL such that A18:
x in proj1 .: (Values G)
and A19:
not
x in proj1 .: (rng (mid (f,k1,k2)))
;
consider p being
Element of
(TOP-REAL 2) such that A20:
p in Values G
and A21:
x = proj1 . p
by A18, FUNCT_2:65;
consider i0,
j0 being
Nat such that A22:
p = G * (
i0,
j0)
and A23:
[i0,j0] in Indices G
by A16, A20;
A24:
i0 <= len G
by A23, MATRIX_0:32;
defpred S1[
Nat]
means ( 1
<= $1 & $1
<= len (mid (f,k1,k2)) implies for
i,
j being
Nat st
[i,j] in Indices G &
G * (
i,
j)
= (mid (f,k1,k2)) . $1 holds
i < i0 );
A25:
1
<= i0
by A23, MATRIX_0:32;
A26:
( 1
<= j0 &
j0 <= width G )
by A23, MATRIX_0:32;
A27:
for
n being
Nat st
S1[
n] holds
S1[
n + 1]
proof
let n be
Nat;
( S1[n] implies S1[n + 1] )
assume that A28:
( 1
<= n &
n <= len (mid (f,k1,k2)) implies for
i,
j being
Nat st
[i,j] in Indices G &
G * (
i,
j)
= (mid (f,k1,k2)) . n holds
i < i0 )
and A29:
1
<= n + 1
and A30:
n + 1
<= len (mid (f,k1,k2))
;
for i, j being Nat st [i,j] in Indices G & G * (i,j) = (mid (f,k1,k2)) . (n + 1) holds
i < i0
let i,
j be
Nat;
( [i,j] in Indices G & G * (i,j) = (mid (f,k1,k2)) . (n + 1) implies i < i0 )
assume that A31:
[i,j] in Indices G
and A32:
G * (
i,
j)
= (mid (f,k1,k2)) . (n + 1)
;
i < i0
A33:
now not i = i0A34:
n + 1
in dom (mid (f,k1,k2))
by A29, A30, FINSEQ_3:25;
then A35:
G * (
i,
j)
= (mid (f,k1,k2)) /. (n + 1)
by A32, PARTFUN1:def 6;
then A36:
(
dom proj1 = the
carrier of
(TOP-REAL 2) &
(mid (f,k1,k2)) /. (n + 1) in rng (mid (f,k1,k2)) )
by A32, A34, FUNCT_1:3, FUNCT_2:def 1;
A37:
( 1
<= j &
j <= width G )
by A31, MATRIX_0:32;
assume A38:
i = i0
;
contradictionx =
p `1
by A21, PSCOMP_1:def 5
.=
(G * (i0,1)) `1
by A22, A25, A24, A26, GOBOARD5:2
.=
(G * (i,j)) `1
by A25, A24, A38, A37, GOBOARD5:2
.=
proj1 . ((mid (f,k1,k2)) /. (n + 1))
by A35, PSCOMP_1:def 5
;
hence
contradiction
by A19, A36, FUNCT_1:def 6;
verum end;
per cases
( n = 0 or n <> 0 )
;
suppose
n = 0
;
i < i0then
G * (
i,
j)
= G * (1,
i1)
by A5, A6, A12, A14, A11, A32, FINSEQ_6:118;
then
i = 1
by A2, A31, Th26;
hence
i < i0
by A25, A33, XXREAL_0:1;
verum end; suppose A39:
n <> 0
;
i < i0then A40:
1
<= n
by NAT_1:14;
A41:
n <= n + 1
by NAT_1:11;
then
n <= len (mid (f,k1,k2))
by A30, XXREAL_0:2;
then A42:
n in dom (mid (f,k1,k2))
by A40, FINSEQ_3:25;
then consider i1,
j1 being
Nat such that A43:
(
[i1,j1] in Indices G &
(mid (f,k1,k2)) /. n = G * (
i1,
j1) )
by A13, GOBOARD1:def 9;
A44:
n + 1
in dom (mid (f,k1,k2))
by A29, A30, FINSEQ_3:25;
then
(mid (f,k1,k2)) /. (n + 1) = G * (
i,
j)
by A32, PARTFUN1:def 6;
then
|.(i1 - i).| + |.(j1 - j).| = 1
by A13, A31, A42, A43, A44, GOBOARD1:def 9;
then A45:
( (
|.(i1 - i).| = 1 &
j1 = j ) or (
|.(j1 - j).| = 1 &
i1 = i ) )
by SEQM_3:42;
now i < i0
(mid (f,k1,k2)) . n = (mid (f,k1,k2)) /. n
by A42, PARTFUN1:def 6;
then A46:
i1 < i0
by A28, A30, A39, A41, A43, NAT_1:14, XXREAL_0:2;
end; hence
i < i0
;
verum end; end;
end;
A47:
G * (
(len G),
i2)
= (mid (f,k1,k2)) . (len (mid (f,k1,k2)))
by A6, A12, A10, A14, A11, JORDAN4:11;
A48:
S1[
0 ]
;
for
n being
Nat holds
S1[
n]
from NAT_1:sch 2(A48, A27);
then
len G < i0
by A7, A15, A47;
hence
contradiction
by A23, MATRIX_0:32;
verum
end;
thus
proj1 .: (rng f) c= proj1 .: (Values G)
by A1, GOBRD13:8, RELAT_1:123; XBOOLE_0:def 10 proj1 .: (Values G) c= proj1 .: (rng f)
proj1 .: (rng (mid (f,k1,k2))) c= proj1 .: (rng f)
by FINSEQ_6:119, RELAT_1:123;
hence
proj1 .: (Values G) c= proj1 .: (rng f)
by A17; verum