let f be non empty FinSequence of (TOP-REAL 2); :: thesis: for G being Go-board st f is_sequence_on G & ex i being Element of NAT st
( [1,i] in Indices G & G * 1,i in rng f ) & ex i being Element of 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; :: thesis: ( f is_sequence_on G & ex i being Element of NAT st
( [1,i] in Indices G & G * 1,i in rng f ) & ex i being Element of 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 ; :: thesis: ( for i being Element of NAT holds
( not [1,i] in Indices G or not G * 1,i in rng f ) or for i being Element of 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 Element of NAT such that A2: [1,i1] in Indices G and
A3: G * 1,i1 in rng f ; :: thesis: ( for i being Element of 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 i2 being Element of NAT such that A4: [(len G),i2] in Indices G and
A5: G * (len G),i2 in rng f ; :: thesis: proj1 .: (rng f) = proj1 .: (Values G)
thus proj1 .: (rng f) c= proj1 .: (Values G) by A1, GOBRD13:9, RELAT_1:156; :: according to XBOOLE_0:def 10 :: thesis: proj1 .: (Values G) c= proj1 .: (rng f)
A6: Values G = { (G * i,j) where i, j is Element of NAT : [i,j] in Indices G } by GOBRD13:7;
consider k1 being set such that
A7: k1 in dom f and
A8: G * 1,i1 = f . k1 by A3, FUNCT_1:def 5;
reconsider k1 = k1 as Element of NAT by A7;
A9: ( 1 <= k1 & k1 <= len f ) by A7, FINSEQ_3:27;
consider k2 being set such that
A10: k2 in dom f and
A11: G * (len G),i2 = f . k2 by A5, FUNCT_1:def 5;
reconsider k2 = k2 as Element of NAT by A10;
A12: ( 1 <= k2 & k2 <= len f ) by A10, FINSEQ_3:27;
set g = mid f,k1,k2;
A13: mid f,k1,k2 is_sequence_on G by A1, Th33;
A14: now
per cases ( k1 <= k2 or k1 > k2 ) ;
suppose k1 <= k2 ; :: thesis: len (mid f,k1,k2) >= 0 + 1
then len (mid f,k1,k2) = (k2 -' k1) + 1 by A9, A12, JORDAN4:20;
hence len (mid f,k1,k2) >= 0 + 1 by XREAL_1:8; :: thesis: verum
end;
suppose k1 > k2 ; :: thesis: len (mid f,k1,k2) >= 0 + 1
then len (mid f,k1,k2) = (k1 -' k2) + 1 by A9, A12, JORDAN4:21;
hence len (mid f,k1,k2) >= 0 + 1 by XREAL_1:8; :: thesis: verum
end;
end;
end;
A15: proj1 .: (Values G) c= proj1 .: (rng (mid f,k1,k2))
proof
assume not proj1 .: (Values G) c= proj1 .: (rng (mid f,k1,k2)) ; :: thesis: contradiction
then consider x being Element of REAL such that
A16: x in proj1 .: (Values G) and
A17: not x in proj1 .: (rng (mid f,k1,k2)) by SUBSET_1:7;
consider p being Element of (TOP-REAL 2) such that
A18: p in Values G and
A19: x = proj1 . p by A16, FUNCT_2:116;
consider i0, j0 being Element of NAT such that
A20: p = G * i0,j0 and
A21: [i0,j0] in Indices G by A6, A18;
A22: ( 1 <= i0 & i0 <= len G ) by A21, MATRIX_1:39;
A23: ( 1 <= j0 & j0 <= width G ) by A21, MATRIX_1:39;
defpred S1[ Nat] means ( 1 <= $1 & $1 <= len (mid f,k1,k2) implies for i, j being Element of NAT st [i,j] in Indices G & G * i,j = (mid f,k1,k2) . $1 holds
i < i0 );
A24: S1[ 0 ] ;
A25: for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
let n be Element of NAT ; :: thesis: ( S1[n] implies S1[n + 1] )
assume that
A26: ( 1 <= n & n <= len (mid f,k1,k2) implies for i, j being Element of NAT st [i,j] in Indices G & G * i,j = (mid f,k1,k2) . n holds
i < i0 ) and
A27: ( 1 <= n + 1 & n + 1 <= len (mid f,k1,k2) ) ; :: thesis: for i, j being Element of NAT st [i,j] in Indices G & G * i,j = (mid f,k1,k2) . (n + 1) holds
i < i0
let i, j be Element of NAT ; :: thesis: ( [i,j] in Indices G & G * i,j = (mid f,k1,k2) . (n + 1) implies i < i0 )
assume that
A28: [i,j] in Indices G and
A29: G * i,j = (mid f,k1,k2) . (n + 1) ; :: thesis: i < i0
A30: now
assume A31: i = i0 ; :: thesis: contradiction
A32: n + 1 in dom (mid f,k1,k2) by A27, FINSEQ_3:27;
then A33: G * i,j = (mid f,k1,k2) /. (n + 1) by A29, PARTFUN1:def 8;
A34: ( 1 <= j & j <= width G ) by A28, MATRIX_1:39;
A35: x = p `1 by A19, PSCOMP_1:def 28
.= (G * i0,1) `1 by A20, A22, A23, GOBOARD5:3
.= (G * i,j) `1 by A22, A31, A34, GOBOARD5:3
.= proj1 . ((mid f,k1,k2) /. (n + 1)) by A33, PSCOMP_1:def 28 ;
A36: dom proj1 = the carrier of (TOP-REAL 2) by FUNCT_2:def 1;
(mid f,k1,k2) /. (n + 1) in rng (mid f,k1,k2) by A29, A32, A33, FUNCT_1:12;
hence contradiction by A17, A35, A36, FUNCT_1:def 12; :: thesis: verum
end;
per cases ( n = 0 or n <> 0 ) ;
suppose n = 0 ; :: thesis: i < i0
then G * i,j = G * 1,i1 by A8, A9, A12, A29, JORDAN3:27;
then i = 1 by A2, A28, Th32;
hence i < i0 by A22, A30, XXREAL_0:1; :: thesis: verum
end;
suppose A37: n <> 0 ; :: thesis: i < i0
then A38: 1 <= n by NAT_1:14;
A39: n <= n + 1 by NAT_1:11;
then n <= len (mid f,k1,k2) by A27, XXREAL_0:2;
then A40: n in dom (mid f,k1,k2) by A38, FINSEQ_3:27;
then consider i1, j1 being Element of NAT such that
A41: [i1,j1] in Indices G and
A42: (mid f,k1,k2) /. n = G * i1,j1 by A13, GOBOARD1:def 11;
A43: n + 1 in dom (mid f,k1,k2) by A27, FINSEQ_3:27;
then (mid f,k1,k2) /. (n + 1) = G * i,j by A29, PARTFUN1:def 8;
then (abs (i1 - i)) + (abs (j1 - j)) = 1 by A13, A28, A40, A41, A42, A43, GOBOARD1:def 11;
then A44: ( ( abs (i1 - i) = 1 & j1 = j ) or ( abs (j1 - j) = 1 & i1 = i ) ) by GOBOARD1:2;
now
(mid f,k1,k2) . n = (mid f,k1,k2) /. n by A40, PARTFUN1:def 8;
then A45: i1 < i0 by A26, A27, A37, A39, A41, A42, NAT_1:14, XXREAL_0:2;
per cases ( i1 = i or i < i1 or i = i1 + 1 ) by A44, GOBOARD1:1;
suppose ( i1 = i or i < i1 ) ; :: thesis: i < i0
hence i < i0 by A45, XXREAL_0:2; :: thesis: verum
end;
end;
end;
hence i < i0 ; :: thesis: verum
end;
end;
end;
A46: for n being Element of NAT holds S1[n] from NAT_1:sch 1(A24, A25);
 G * (len G),i2 = (mid f,k1,k2) . (len (mid f,k1,k2)) by A9, A11, A12, JORDAN4:23;
then len G < i0 by A4, A14, A46;
hence contradiction by A21, MATRIX_1:39; :: thesis: verum
end;
proj1 .: (rng (mid f,k1,k2)) c= proj1 .: (rng f) by JORDAN3:28, RELAT_1:156;
hence proj1 .: (Values G) c= proj1 .: (rng f) by A15, XBOOLE_1:1; :: thesis: verum