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
( [i,1] in Indices G & G * i,1 in rng f ) & ex i being Element of NAT st
( [i,(width G)] in Indices G & G * i,(width G) in rng f ) holds
proj2 .: (rng f) = proj2 .: (Values G)
let G be Go-board; :: thesis: ( f is_sequence_on G & ex i being Element of NAT st
( [i,1] in Indices G & G * i,1 in rng f ) & ex i being Element of NAT st
( [i,(width G)] in Indices G & G * i,(width G) in rng f ) implies proj2 .: (rng f) = proj2 .: (Values G) )
assume A1: f is_sequence_on G ; :: thesis: ( for i being Element of NAT holds
( not [i,1] in Indices G or not G * i,1 in rng f ) or for i being Element of NAT holds
( not [i,(width G)] in Indices G or not G * i,(width G) in rng f ) or proj2 .: (rng f) = proj2 .: (Values G) )
given i1 being Element of NAT such that A2: [i1,1] in Indices G and
A3: G * i1,1 in rng f ; :: thesis: ( for i being Element of NAT holds
( not [i,(width G)] in Indices G or not G * i,(width G) in rng f ) or proj2 .: (rng f) = proj2 .: (Values G) )
consider k1 being set such that
A4: k1 in dom f and
A5: G * i1,1 = f . k1 by A3, FUNCT_1:def 5;
reconsider k1 = k1 as Element of NAT by A4;
A6: 1 <= k1 by A4, FINSEQ_3:27;
given i2 being Element of NAT such that A7: [i2,(width G)] in Indices G and
A8: G * i2,(width G) in rng f ; :: thesis: proj2 .: (rng f) = proj2 .: (Values G)
consider k2 being set such that
A9: k2 in dom f and
A10: G * i2,(width G) = f . k2 by A8, FUNCT_1:def 5;
reconsider k2 = k2 as Element of NAT by A9;
A11: k2 <= len f by A9, FINSEQ_3:27;
A12: k1 <= len f by A4, FINSEQ_3:27;
set g = mid f,k1,k2;
A13: mid f,k1,k2 is_sequence_on G by A1, Th33;
A14: 1 <= k2 by A9, FINSEQ_3:27;

A15: 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 A6, A11, 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 A12, A14, JORDAN4:21;
hence len (mid f,k1,k2) >= 0 + 1 by XREAL_1:8; :: thesis: verum

end;

end;

end;

A16: Values G = { (G * i,j) where i, j is Element of NAT : [i,j] in Indices G } by GOBRD13:7;
A17: proj2 .: (Values G) c= proj2 .: (rng (mid f,k1,k2))

proof

assume not proj2 .: (Values G) c= proj2 .: (rng (mid f,k1,k2)) ; :: thesis: contradiction
then consider x being Element of REAL such that
A18: x in proj2 .: (Values G) and
A19: not x in proj2 .: (rng (mid f,k1,k2)) by SUBSET_1:7;
consider p being Element of (TOP-REAL 2) such that
A20: p in Values G and
A21: x = proj2 . p by A18, FUNCT_2:116;
consider i0, j0 being Element of NAT such that
A22: p = G * i0,j0 and
A23: [i0,j0] in Indices G by A16, A20;
A24: j0 <= width G by A23, MATRIX_1:39;
defpred S₁[ 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
j < j0 );
A25: 1 <= j0 by A23, MATRIX_1:39;
A26: ( 1 <= i0 & i0 <= len G ) by A23, MATRIX_1:39;
A27: for n being Element of NAT st S₁[n] holds
S₁[n + 1]

proof

let n be Element of NAT ; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume that
A28: ( 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
j < j0 ) and
A29: 1 <= n + 1 and
A30: 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
j < j0
let i, j be Element of NAT ; :: thesis: ( [i,j] in Indices G & G * i,j = (mid f,k1,k2) . (n + 1) implies j < j0 )
assume that
A31: [i,j] in Indices G and
A32: G * i,j = (mid f,k1,k2) . (n + 1) ; :: thesis: j < j0

A33: now

A34: n + 1 in dom (mid f,k1,k2) by A29, A30, FINSEQ_3:27;
then A35: G * i,j = (mid f,k1,k2) /. (n + 1) by A32, PARTFUN1:def 8;
then A36: ( dom proj2 = the carrier of (TOP-REAL 2) & (mid f,k1,k2) /. (n + 1) in rng (mid f,k1,k2) ) by A32, A34, FUNCT_1:12, FUNCT_2:def 1;
A37: ( 1 <= i & i <= len G ) by A31, MATRIX_1:39;
assume A38: j = j0 ; :: thesis: contradiction
x = p `2 by A21, PSCOMP_1:def 29
.= (G * 1,j0) `2 by A22, A26, A25, A24, GOBOARD5:2
.= (G * i,j) `2 by A25, A24, A38, A37, GOBOARD5:2
.= proj2 . ((mid f,k1,k2) /. (n + 1)) by A35, PSCOMP_1:def 29 ;
hence contradiction by A19, A36, FUNCT_1:def 12; :: thesis: verum

end;

per cases ( n = 0 or n <> 0 ) ;

suppose n = 0 ; :: thesis: j < j0

then G * i,j = G * i1,1 by A5, A6, A12, A14, A11, A32, JORDAN3:27;
then j = 1 by A2, A31, Th32;
hence j < j0 by A25, A33, XXREAL_0:1; :: thesis: verum

end;

suppose A39: n <> 0 ; :: thesis: j < j0

then 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:27;
then consider i1, j1 being Element of NAT such that
A43: ( [i1,j1] in Indices G & (mid f,k1,k2) /. n = G * i1,j1 ) by A13, GOBOARD1:def 11;
A44: n + 1 in dom (mid f,k1,k2) by A29, A30, FINSEQ_3:27;
then (mid f,k1,k2) /. (n + 1) = G * i,j by A32, PARTFUN1:def 8;
then (abs (i1 - i)) + (abs (j1 - j)) = 1 by A13, A31, A42, A43, A44, GOBOARD1:def 11;
then A45: ( ( 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 A42, PARTFUN1:def 8;
then A46: j1 < j0 by A28, A30, A39, A41, A43, NAT_1:14, XXREAL_0:2;

per cases ( j1 = j or j < j1 or j = j1 + 1 ) by A45, GOBOARD1:1;

suppose ( j1 = j or j < j1 ) ; :: thesis: j < j0

hence j < j0 by A46, XXREAL_0:2; :: thesis: verum

end;

suppose j = j1 + 1 ; :: thesis: j < j0

then j <= j0 by A46, NAT_1:13;
hence j < j0 by A33, XXREAL_0:1; :: thesis: verum

end;

end;

end;

hence j < j0 ; :: thesis: verum

end;

end;

end;

A47: G * i2,(width G) = (mid f,k1,k2) . (len (mid f,k1,k2)) by A6, A12, A10, A14, A11, JORDAN4:23;
A48: S₁[ 0 ] ;
for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A48, A27);
then width G < j0 by A7, A15, A47;
hence contradiction by A23, MATRIX_1:39; :: thesis: verum

end;

thus proj2 .: (rng f) c= proj2 .: (Values G) by A1, GOBRD13:9, RELAT_1:156; :: according to XBOOLE_0:def 10 :: thesis: proj2 .: (Values G) c= proj2 .: (rng f)
proj2 .: (rng (mid f,k1,k2)) c= proj2 .: (rng f) by JORDAN3:28, RELAT_1:156;
hence proj2 .: (Values G) c= proj2 .: (rng f) by A17, XBOOLE_1:1; :: thesis: verum