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 Nat st
( [i,1] in Indices G & G * (i,1) in rng f ) & ex i being 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 Nat st
( [i,1] in Indices G & G * (i,1) in rng f ) & ex i being 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 Nat holds
( not [i,1] in Indices G or not G * (i,1) in rng f ) or for i being 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 Nat such that A2: [i1,1] in Indices G and
A3: G * (i1,1) in rng f ; :: thesis: ( for i being 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 object such that
A4: k1 in dom f and
A5: G * (i1,1) = 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: [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 object such that
A9: k2 in dom f and
A10: G * (i2,(width G)) = 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;
A15: now :: thesis: len (mid (f,k1,k2)) >= 0 + 1
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, FINSEQ_6:186;
hence len (mid (f,k1,k2)) >= 0 + 1 by XREAL_1:6; :: 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, FINSEQ_6:187;
hence len (mid (f,k1,k2)) >= 0 + 1 by XREAL_1:6; :: thesis: verum
end;
end;
end;
A16: Values G = { (G * (i,j)) where i, j is Nat : [i,j] in Indices G } by MATRIX_0:39;
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))) ;
consider p being Element of (TOP-REAL 2) such that
A20: p in Values G and
A21: x = proj2 . 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: j0 <= width 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
j < j0 );
A25: 1 <= j0 by A23, MATRIX_0:32;
A26: ( 1 <= i0 & i0 <= len G ) by A23, MATRIX_0:32;
A27: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( 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
j < j0 ) and
A29: 1 <= n + 1 and
A30: n + 1 <= len (mid (f,k1,k2)) ; :: thesis: for i, j being Nat st [i,j] in Indices G & G * (i,j) = (mid (f,k1,k2)) . (n + 1) holds
j < j0
let i, j be 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 :: thesis: not j = j0
A34: 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 proj2 = 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 <= i & i <= len G ) by A31, MATRIX_0:32;
assume A38: j = j0 ; :: thesis: contradiction
x = p `2 by A21, PSCOMP_1:def 6
.= (G * (1,j0)) `2 by A22, A26, A25, A24, GOBOARD5:1
.= (G * (i,j)) `2 by A25, A24, A38, A37, GOBOARD5:1
.= proj2 . ((mid (f,k1,k2)) /. (n + 1)) by A35, PSCOMP_1:def 6 ;
hence contradiction by A19, A36, FUNCT_1:def 6; :: 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, FINSEQ_6:118;
then j = 1 by A2, A31, Th26;
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: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 :: thesis: j < j0
(mid (f,k1,k2)) . n = (mid (f,k1,k2)) /. n by A42, PARTFUN1:def 6;
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, SEQM_3:41;
suppose ( j1 = j or j < j1 ) ; :: thesis: j < j0
hence j < j0 by A46, XXREAL_0:2; :: 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, FINSEQ_6:189;
A48: S1[ 0 ] ;
for n being Nat holds S1[n] from NAT_1:sch 2(A48, A27);
 then width G < j0 by A7, A15, A47;
hence contradiction by A23, MATRIX_0:32; :: thesis: verum
end;
thus proj2 .: (rng f) c= proj2 .: (Values G) by A1, GOBRD13:8, RELAT_1:123; :: 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 FINSEQ_6:119, RELAT_1:123;
hence proj2 .: (Values G) c= proj2 .: (rng f) by A17; :: thesis: verum