:: GOBOARD1 semantic presentation
begin
definition
let f be FinSequence of (TOP-REAL 2);
func X_axis f -> FinSequence of REAL means :Def1: :: GOBOARD1:def 1
( len it = len f & ( for n being Element of NAT st n in dom it holds
it . n = (f /. n) `1 ) );
existence
ex b1 being FinSequence of REAL st
( len b1 = len f & ( for n being Element of NAT st n in dom b1 holds
b1 . n = (f /. n) `1 ) )
proof
defpred S1[ Nat, set ] means $2 = (f /. $1) `1 ;
A1: for k being Nat st k in Seg (len f) holds
ex r being Real st S1[k,r] ;
consider v being FinSequence of REAL such that
A2: dom v = Seg (len f) and
A3: for k being Nat st k in Seg (len f) holds
S1[k,v . k] from FINSEQ_1:sch_5(A1);
take v ; ::_thesis: ( len v = len f & ( for n being Element of NAT st n in dom v holds
v . n = (f /. n) `1 ) )
thus len v = len f by A2, FINSEQ_1:def_3; ::_thesis: for n being Element of NAT st n in dom v holds
v . n = (f /. n) `1
let n be Element of NAT ; ::_thesis: ( n in dom v implies v . n = (f /. n) `1 )
assume n in dom v ; ::_thesis: v . n = (f /. n) `1
hence v . n = (f /. n) `1 by A2, A3; ::_thesis: verum
end;
uniqueness
for b1, b2 being FinSequence of REAL st len b1 = len f & ( for n being Element of NAT st n in dom b1 holds
b1 . n = (f /. n) `1 ) & len b2 = len f & ( for n being Element of NAT st n in dom b2 holds
b2 . n = (f /. n) `1 ) holds
b1 = b2
proof
let v1, v2 be FinSequence of REAL ; ::_thesis: ( len v1 = len f & ( for n being Element of NAT st n in dom v1 holds
v1 . n = (f /. n) `1 ) & len v2 = len f & ( for n being Element of NAT st n in dom v2 holds
v2 . n = (f /. n) `1 ) implies v1 = v2 )
assume that
A4: len v1 = len f and
A5: for n being Element of NAT st n in dom v1 holds
v1 . n = (f /. n) `1 and
A6: len v2 = len f and
A7: for n being Element of NAT st n in dom v2 holds
v2 . n = (f /. n) `1 ; ::_thesis: v1 = v2
A8: dom v2 = Seg (len v2) by FINSEQ_1:def_3;
A9: dom f = Seg (len f) by FINSEQ_1:def_3;
A10: dom v1 = Seg (len v1) by FINSEQ_1:def_3;
now__::_thesis:_for_n_being_Nat_st_n_in_dom_f_holds_
v1_._n_=_v2_._n
let n be Nat; ::_thesis: ( n in dom f implies v1 . n = v2 . n )
assume A11: n in dom f ; ::_thesis: v1 . n = v2 . n
hence v1 . n = (f /. n) `1 by A4, A5, A10, A9
.= v2 . n by A6, A7, A8, A9, A11 ;
::_thesis: verum
end;
hence v1 = v2 by A4, A6, A10, A8, A9, FINSEQ_1:13; ::_thesis: verum
end;
func Y_axis f -> FinSequence of REAL means :Def2: :: GOBOARD1:def 2
( len it = len f & ( for n being Element of NAT st n in dom it holds
it . n = (f /. n) `2 ) );
existence
ex b1 being FinSequence of REAL st
( len b1 = len f & ( for n being Element of NAT st n in dom b1 holds
b1 . n = (f /. n) `2 ) )
proof
defpred S1[ Nat, set ] means $2 = (f /. $1) `2 ;
A12: for k being Nat st k in Seg (len f) holds
ex r being Real st S1[k,r] ;
consider v being FinSequence of REAL such that
A13: dom v = Seg (len f) and
A14: for k being Nat st k in Seg (len f) holds
S1[k,v . k] from FINSEQ_1:sch_5(A12);
take v ; ::_thesis: ( len v = len f & ( for n being Element of NAT st n in dom v holds
v . n = (f /. n) `2 ) )
thus len v = len f by A13, FINSEQ_1:def_3; ::_thesis: for n being Element of NAT st n in dom v holds
v . n = (f /. n) `2
let n be Element of NAT ; ::_thesis: ( n in dom v implies v . n = (f /. n) `2 )
assume n in dom v ; ::_thesis: v . n = (f /. n) `2
hence v . n = (f /. n) `2 by A13, A14; ::_thesis: verum
end;
uniqueness
for b1, b2 being FinSequence of REAL st len b1 = len f & ( for n being Element of NAT st n in dom b1 holds
b1 . n = (f /. n) `2 ) & len b2 = len f & ( for n being Element of NAT st n in dom b2 holds
b2 . n = (f /. n) `2 ) holds
b1 = b2
proof
let v1, v2 be FinSequence of REAL ; ::_thesis: ( len v1 = len f & ( for n being Element of NAT st n in dom v1 holds
v1 . n = (f /. n) `2 ) & len v2 = len f & ( for n being Element of NAT st n in dom v2 holds
v2 . n = (f /. n) `2 ) implies v1 = v2 )
assume that
A15: len v1 = len f and
A16: for n being Element of NAT st n in dom v1 holds
v1 . n = (f /. n) `2 and
A17: len v2 = len f and
A18: for n being Element of NAT st n in dom v2 holds
v2 . n = (f /. n) `2 ; ::_thesis: v1 = v2
A19: dom v2 = Seg (len v2) by FINSEQ_1:def_3;
A20: dom f = Seg (len f) by FINSEQ_1:def_3;
A21: dom v1 = Seg (len v1) by FINSEQ_1:def_3;
now__::_thesis:_for_n_being_Nat_st_n_in_dom_f_holds_
v1_._n_=_v2_._n
let n be Nat; ::_thesis: ( n in dom f implies v1 . n = v2 . n )
assume A22: n in dom f ; ::_thesis: v1 . n = v2 . n
hence v1 . n = (f /. n) `2 by A15, A16, A21, A20
.= v2 . n by A17, A18, A19, A20, A22 ;
::_thesis: verum
end;
hence v1 = v2 by A15, A17, A21, A19, A20, FINSEQ_1:13; ::_thesis: verum
end;
end;
:: deftheorem Def1 defines X_axis GOBOARD1:def_1_:_
for f being FinSequence of (TOP-REAL 2)
for b2 being FinSequence of REAL holds
( b2 = X_axis f iff ( len b2 = len f & ( for n being Element of NAT st n in dom b2 holds
b2 . n = (f /. n) `1 ) ) );
:: deftheorem Def2 defines Y_axis GOBOARD1:def_2_:_
for f being FinSequence of (TOP-REAL 2)
for b2 being FinSequence of REAL holds
( b2 = Y_axis f iff ( len b2 = len f & ( for n being Element of NAT st n in dom b2 holds
b2 . n = (f /. n) `2 ) ) );
theorem Th1: :: GOBOARD1:1
for f being FinSequence of (TOP-REAL 2)
for i being Element of NAT st i in dom f & 2 <= len f holds
f /. i in L~ f
proof
let f be FinSequence of (TOP-REAL 2); ::_thesis: for i being Element of NAT st i in dom f & 2 <= len f holds
f /. i in L~ f
let i be Element of NAT ; ::_thesis: ( i in dom f & 2 <= len f implies f /. i in L~ f )
assume that
A1: i in dom f and
A2: 2 <= len f ; ::_thesis: f /. i in L~ f
A3: 1 <= i by A1, FINSEQ_3:25;
A4: i <= len f by A1, FINSEQ_3:25;
percases ( i = len f or i < len f ) by A4, XXREAL_0:1;
supposeA5: i = len f ; ::_thesis: f /. i in L~ f
reconsider l = i - 1 as Element of NAT by A3, INT_1:5;
1 + 1 <= i by A2, A5;
then 1 <= l by XREAL_1:19;
then A6: f /. (l + 1) in LSeg (f,l) by A4, TOPREAL1:21;
LSeg (f,l) c= L~ f by TOPREAL3:19;
hence f /. i in L~ f by A6; ::_thesis: verum
end;
suppose i < len f ; ::_thesis: f /. i in L~ f
then i + 1 <= len f by NAT_1:13;
then A7: f /. i in LSeg (f,i) by A3, TOPREAL1:21;
LSeg (f,i) c= L~ f by TOPREAL3:19;
hence f /. i in L~ f by A7; ::_thesis: verum
end;
end;
end;
begin
theorem Th2: :: GOBOARD1:2
for D being non empty set
for M being Matrix of D
for i, j being Element of NAT st j in dom M & i in Seg (width M) holds
(Col (M,i)) . j = (Line (M,j)) . i
proof
let D be non empty set ; ::_thesis: for M being Matrix of D
for i, j being Element of NAT st j in dom M & i in Seg (width M) holds
(Col (M,i)) . j = (Line (M,j)) . i
let M be Matrix of D; ::_thesis: for i, j being Element of NAT st j in dom M & i in Seg (width M) holds
(Col (M,i)) . j = (Line (M,j)) . i
let i, j be Element of NAT ; ::_thesis: ( j in dom M & i in Seg (width M) implies (Col (M,i)) . j = (Line (M,j)) . i )
assume that
A1: j in dom M and
A2: i in Seg (width M) ; ::_thesis: (Col (M,i)) . j = (Line (M,j)) . i
thus (Col (M,i)) . j = M * (j,i) by A1, MATRIX_1:def_8
.= (Line (M,j)) . i by A2, MATRIX_1:def_7 ; ::_thesis: verum
end;
definition
let D be non empty set ;
let M be Matrix of D;
:: original: empty-yielding
redefine attrM is empty-yielding means :Def3: :: GOBOARD1:def 3
( 0 = len M or 0 = width M );
compatibility
( M is empty-yielding iff ( 0 = len M or 0 = width M ) )
proof
consider n being Nat such that
A1: for x being set st x in rng M holds
ex s being FinSequence st
( s = x & len s = n ) by MATRIX_1:def_1;
hereby ::_thesis: ( ( 0 = len M or 0 = width M ) implies M is empty-yielding )
set s = the Element of rng M;
assume A2: M is empty-yielding ; ::_thesis: ( 0 <> len M implies 0 = width M )
assume A3: 0 <> len M ; ::_thesis: 0 = width M
then A4: M <> {} ;
then ex p being FinSequence st
( p = the Element of rng M & len p = n ) by A1;
then reconsider s = the Element of rng M as FinSequence ;
s = 0 by A2, A4, RELAT_1:149;
hence 0 = width M by A3, A4, CARD_1:27, MATRIX_1:def_3; ::_thesis: verum
end;
assume A5: ( 0 = len M or 0 = width M ) ; ::_thesis: M is empty-yielding
now__::_thesis:_for_s_being_set_st_s_in_rng_M_holds_
s_=_{}
let s be set ; ::_thesis: ( s in rng M implies s = {} )
assume A6: s in rng M ; ::_thesis: s = {}
then M <> {} ;
then len M > 0 ;
then consider p being FinSequence such that
A7: p in rng M and
A8: len p = 0 by A5, MATRIX_1:def_3;
ex q being FinSequence st
( q = p & len q = n ) by A1, A7;
then ex q being FinSequence st
( q = s & len q = 0 ) by A1, A6, A8;
hence s = {} ; ::_thesis: verum
end;
hence M is empty-yielding by RELAT_1:149; ::_thesis: verum
end;
end;
:: deftheorem Def3 defines empty-yielding GOBOARD1:def_3_:_
for D being non empty set
for M being Matrix of D holds
( M is empty-yielding iff ( 0 = len M or 0 = width M ) );
definition
let M be Matrix of (TOP-REAL 2);
attrM is X_equal-in-line means :Def4: :: GOBOARD1:def 4
for n being Element of NAT st n in dom M holds
X_axis (Line (M,n)) is constant ;
attrM is Y_equal-in-column means :Def5: :: GOBOARD1:def 5
for n being Element of NAT st n in Seg (width M) holds
Y_axis (Col (M,n)) is constant ;
attrM is Y_increasing-in-line means :Def6: :: GOBOARD1:def 6
for n being Element of NAT st n in dom M holds
Y_axis (Line (M,n)) is increasing ;
attrM is X_increasing-in-column means :Def7: :: GOBOARD1:def 7
for n being Element of NAT st n in Seg (width M) holds
X_axis (Col (M,n)) is increasing ;
end;
:: deftheorem Def4 defines X_equal-in-line GOBOARD1:def_4_:_
for M being Matrix of (TOP-REAL 2) holds
( M is X_equal-in-line iff for n being Element of NAT st n in dom M holds
X_axis (Line (M,n)) is constant );
:: deftheorem Def5 defines Y_equal-in-column GOBOARD1:def_5_:_
for M being Matrix of (TOP-REAL 2) holds
( M is Y_equal-in-column iff for n being Element of NAT st n in Seg (width M) holds
Y_axis (Col (M,n)) is constant );
:: deftheorem Def6 defines Y_increasing-in-line GOBOARD1:def_6_:_
for M being Matrix of (TOP-REAL 2) holds
( M is Y_increasing-in-line iff for n being Element of NAT st n in dom M holds
Y_axis (Line (M,n)) is increasing );
:: deftheorem Def7 defines X_increasing-in-column GOBOARD1:def_7_:_
for M being Matrix of (TOP-REAL 2) holds
( M is X_increasing-in-column iff for n being Element of NAT st n in Seg (width M) holds
X_axis (Col (M,n)) is increasing );
Lm1: for D being non empty set
for M being Matrix of D holds
( M is V3() iff ( 0 < len M & 0 < width M ) )
proof
let D be non empty set ; ::_thesis: for M being Matrix of D holds
( M is V3() iff ( 0 < len M & 0 < width M ) )
let M be Matrix of D; ::_thesis: ( M is V3() iff ( 0 < len M & 0 < width M ) )
hereby ::_thesis: ( 0 < len M & 0 < width M implies not M is V3() )
assume M is V3() ; ::_thesis: ( 0 < len M & 0 < width M )
then ( 0 <> len M & 0 <> width M ) by Def3;
hence ( 0 < len M & 0 < width M ) ; ::_thesis: verum
end;
assume ( 0 < len M & 0 < width M ) ; ::_thesis: M is V3()
hence M is V3() by Def3; ::_thesis: verum
end;
registration
cluster Relation-like V3() NAT -defined K196( the carrier of (TOP-REAL 2)) -valued Function-like V46() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column for FinSequence of K196( the carrier of (TOP-REAL 2));
existence
ex b1 being Matrix of (TOP-REAL 2) st
( b1 is V3() & b1 is X_equal-in-line & b1 is Y_equal-in-column & b1 is Y_increasing-in-line & b1 is X_increasing-in-column )
proof
set p = the Point of (TOP-REAL 2);
take M = <*<* the Point of (TOP-REAL 2)*>*>; ::_thesis: ( M is V3() & M is X_equal-in-line & M is Y_equal-in-column & M is Y_increasing-in-line & M is X_increasing-in-column )
A1: len M = 1 by MATRIX_1:24;
A2: width M = 1 by MATRIX_1:24;
hence M is V3() by A1, Def3; ::_thesis: ( M is X_equal-in-line & M is Y_equal-in-column & M is Y_increasing-in-line & M is X_increasing-in-column )
thus M is X_equal-in-line ::_thesis: ( M is Y_equal-in-column & M is Y_increasing-in-line & M is X_increasing-in-column )
proof
let n be Element of NAT ; :: according to GOBOARD1:def_4 ::_thesis: ( n in dom M implies X_axis (Line (M,n)) is constant )
assume n in dom M ; ::_thesis: X_axis (Line (M,n)) is constant
set L = X_axis (Line (M,n));
let k be Element of NAT ; :: according to SEQM_3:def_10 ::_thesis: for b1 being Element of NAT holds
( not k in dom (X_axis (Line (M,n))) or not b1 in dom (X_axis (Line (M,n))) or (X_axis (Line (M,n))) . k = (X_axis (Line (M,n))) . b1 )
let m be Element of NAT ; ::_thesis: ( not k in dom (X_axis (Line (M,n))) or not m in dom (X_axis (Line (M,n))) or (X_axis (Line (M,n))) . k = (X_axis (Line (M,n))) . m )
assume that
A3: k in dom (X_axis (Line (M,n))) and
A4: m in dom (X_axis (Line (M,n))) ; ::_thesis: (X_axis (Line (M,n))) . k = (X_axis (Line (M,n))) . m
A5: len (X_axis (Line (M,n))) = len (Line (M,n)) by Def1;
k in Seg (len (X_axis (Line (M,n)))) by A3, FINSEQ_1:def_3;
then k in {1} by A2, A5, FINSEQ_1:2, MATRIX_1:def_7;
then A6: k = 1 by TARSKI:def_1;
m in Seg (len (X_axis (Line (M,n)))) by A4, FINSEQ_1:def_3;
then m in {1} by A2, A5, FINSEQ_1:2, MATRIX_1:def_7;
hence (X_axis (Line (M,n))) . k = (X_axis (Line (M,n))) . m by A6, TARSKI:def_1; ::_thesis: verum
end;
thus M is Y_equal-in-column ::_thesis: ( M is Y_increasing-in-line & M is X_increasing-in-column )
proof
let n be Element of NAT ; :: according to GOBOARD1:def_5 ::_thesis: ( n in Seg (width M) implies Y_axis (Col (M,n)) is constant )
assume n in Seg (width M) ; ::_thesis: Y_axis (Col (M,n)) is constant
set L = Y_axis (Col (M,n));
let k be Element of NAT ; :: according to SEQM_3:def_10 ::_thesis: for b1 being Element of NAT holds
( not k in dom (Y_axis (Col (M,n))) or not b1 in dom (Y_axis (Col (M,n))) or (Y_axis (Col (M,n))) . k = (Y_axis (Col (M,n))) . b1 )
let m be Element of NAT ; ::_thesis: ( not k in dom (Y_axis (Col (M,n))) or not m in dom (Y_axis (Col (M,n))) or (Y_axis (Col (M,n))) . k = (Y_axis (Col (M,n))) . m )
assume that
A7: k in dom (Y_axis (Col (M,n))) and
A8: m in dom (Y_axis (Col (M,n))) ; ::_thesis: (Y_axis (Col (M,n))) . k = (Y_axis (Col (M,n))) . m
A9: len (Y_axis (Col (M,n))) = len (Col (M,n)) by Def2;
k in Seg (len (Y_axis (Col (M,n)))) by A7, FINSEQ_1:def_3;
then k in {1} by A1, A9, FINSEQ_1:2, MATRIX_1:def_8;
then A10: k = 1 by TARSKI:def_1;
m in Seg (len (Y_axis (Col (M,n)))) by A8, FINSEQ_1:def_3;
then m in {1} by A1, A9, FINSEQ_1:2, MATRIX_1:def_8;
hence (Y_axis (Col (M,n))) . k = (Y_axis (Col (M,n))) . m by A10, TARSKI:def_1; ::_thesis: verum
end;
thus M is Y_increasing-in-line ::_thesis: M is X_increasing-in-column
proof
let n be Element of NAT ; :: according to GOBOARD1:def_6 ::_thesis: ( n in dom M implies Y_axis (Line (M,n)) is increasing )
assume n in dom M ; ::_thesis: Y_axis (Line (M,n)) is increasing
set L = Y_axis (Line (M,n));
let k be Element of NAT ; :: according to SEQM_3:def_1 ::_thesis: for b1 being Element of NAT holds
( not k in dom (Y_axis (Line (M,n))) or not b1 in dom (Y_axis (Line (M,n))) or b1 <= k or not (Y_axis (Line (M,n))) . b1 <= (Y_axis (Line (M,n))) . k )
let m be Element of NAT ; ::_thesis: ( not k in dom (Y_axis (Line (M,n))) or not m in dom (Y_axis (Line (M,n))) or m <= k or not (Y_axis (Line (M,n))) . m <= (Y_axis (Line (M,n))) . k )
assume that
A11: k in dom (Y_axis (Line (M,n))) and
A12: m in dom (Y_axis (Line (M,n))) and
A13: k < m ; ::_thesis: not (Y_axis (Line (M,n))) . m <= (Y_axis (Line (M,n))) . k
A14: len (Y_axis (Line (M,n))) = len (Line (M,n)) by Def2;
k in Seg (len (Y_axis (Line (M,n)))) by A11, FINSEQ_1:def_3;
then k in {1} by A2, A14, FINSEQ_1:2, MATRIX_1:def_7;
then A15: k = 1 by TARSKI:def_1;
m in Seg (len (Y_axis (Line (M,n)))) by A12, FINSEQ_1:def_3;
then m in {1} by A2, A14, FINSEQ_1:2, MATRIX_1:def_7;
hence not (Y_axis (Line (M,n))) . m <= (Y_axis (Line (M,n))) . k by A13, A15, TARSKI:def_1; ::_thesis: verum
end;
let n be Element of NAT ; :: according to GOBOARD1:def_7 ::_thesis: ( n in Seg (width M) implies X_axis (Col (M,n)) is increasing )
assume n in Seg (width M) ; ::_thesis: X_axis (Col (M,n)) is increasing
set L = X_axis (Col (M,n));
let k be Element of NAT ; :: according to SEQM_3:def_1 ::_thesis: for b1 being Element of NAT holds
( not k in dom (X_axis (Col (M,n))) or not b1 in dom (X_axis (Col (M,n))) or b1 <= k or not (X_axis (Col (M,n))) . b1 <= (X_axis (Col (M,n))) . k )
let m be Element of NAT ; ::_thesis: ( not k in dom (X_axis (Col (M,n))) or not m in dom (X_axis (Col (M,n))) or m <= k or not (X_axis (Col (M,n))) . m <= (X_axis (Col (M,n))) . k )
assume that
A16: k in dom (X_axis (Col (M,n))) and
A17: m in dom (X_axis (Col (M,n))) and
A18: k < m ; ::_thesis: not (X_axis (Col (M,n))) . m <= (X_axis (Col (M,n))) . k
A19: len (X_axis (Col (M,n))) = len (Col (M,n)) by Def1;
k in Seg (len (X_axis (Col (M,n)))) by A16, FINSEQ_1:def_3;
then k in {1} by A1, A19, FINSEQ_1:2, MATRIX_1:def_8;
then A20: k = 1 by TARSKI:def_1;
m in Seg (len (X_axis (Col (M,n)))) by A17, FINSEQ_1:def_3;
then m in {1} by A1, A19, FINSEQ_1:2, MATRIX_1:def_8;
hence not (X_axis (Col (M,n))) . m <= (X_axis (Col (M,n))) . k by A18, A20, TARSKI:def_1; ::_thesis: verum
end;
end;
theorem Th3: :: GOBOARD1:3
for M being X_equal-in-line X_increasing-in-column Matrix of (TOP-REAL 2)
for x being set
for n, m being Element of NAT st x in rng (Line (M,n)) & x in rng (Line (M,m)) & n in dom M & m in dom M holds
n = m
proof
let M be X_equal-in-line X_increasing-in-column Matrix of (TOP-REAL 2); ::_thesis: for x being set
for n, m being Element of NAT st x in rng (Line (M,n)) & x in rng (Line (M,m)) & n in dom M & m in dom M holds
n = m
assume ex x being set ex n, m being Element of NAT st
( x in rng (Line (M,n)) & x in rng (Line (M,m)) & n in dom M & m in dom M & not n = m ) ; ::_thesis: contradiction
then consider x being set , n, m being Element of NAT such that
A1: x in rng (Line (M,n)) and
A2: x in rng (Line (M,m)) and
A3: n in dom M and
A4: m in dom M and
A5: n <> m ;
A6: ( n < m or m < n ) by A5, XXREAL_0:1;
A7: X_axis (Line (M,m)) is constant by A4, Def4;
reconsider Ln = Line (M,n), Lm = Line (M,m) as FinSequence of (TOP-REAL 2) ;
consider i being Nat such that
A8: i in dom Ln and
A9: Ln . i = x by A1, FINSEQ_2:10;
set C = X_axis (Col (M,i));
A10: len Ln = width M by MATRIX_1:def_7;
reconsider Mi = Col (M,i) as FinSequence of (TOP-REAL 2) ;
A11: (Col (M,i)) . n = M * (n,i) by A3, MATRIX_1:def_8;
A12: len (Col (M,i)) = len M by MATRIX_1:def_8;
then n in dom (Col (M,i)) by A3, FINSEQ_3:29;
then A13: M * (n,i) = Mi /. n by A11, PARTFUN1:def_6;
A14: (Col (M,i)) . m = M * (m,i) by A4, MATRIX_1:def_8;
A15: dom M = Seg (len M) by FINSEQ_1:def_3;
then m in dom (Col (M,i)) by A4, A12, FINSEQ_1:def_3;
then A16: M * (m,i) = Mi /. m by A14, PARTFUN1:def_6;
consider j being Nat such that
A17: j in dom Lm and
A18: Lm . j = x by A2, FINSEQ_2:10;
A19: ( len (X_axis (Col (M,i))) = len (Col (M,i)) & dom (X_axis (Col (M,i))) = Seg (len (X_axis (Col (M,i)))) ) by Def1, FINSEQ_1:def_3;
A20: Seg (len Ln) = dom Ln by FINSEQ_1:def_3;
then A21: X_axis (Col (M,i)) is increasing by A8, A10, Def7;
A22: len Lm = width M by MATRIX_1:def_7;
then A23: i in dom Lm by A8, A10, FINSEQ_3:29;
Lm . i = M * (m,i) by A8, A10, A20, MATRIX_1:def_7;
then A24: Lm /. i = M * (m,i) by A23, PARTFUN1:def_6;
A25: dom (X_axis Lm) = Seg (len (X_axis Lm)) by FINSEQ_1:def_3;
Ln . i = M * (n,i) by A8, A10, A20, MATRIX_1:def_7;
then reconsider p = x as Point of (TOP-REAL 2) by A9;
A26: Lm /. j = p by A17, A18, PARTFUN1:def_6;
A27: len (X_axis Lm) = len Lm by Def1;
then A28: j in dom (X_axis Lm) by A17, FINSEQ_3:29;
Seg (len Lm) = dom Lm by FINSEQ_1:def_3;
then A29: j in dom (X_axis Lm) by A17, A25, Def1;
i in dom (X_axis Lm) by A8, A10, A22, A27, FINSEQ_3:29;
then (X_axis Lm) . i = (X_axis Lm) . j by A7, A28, SEQM_3:def_10;
then A30: (M * (m,i)) `1 = (X_axis Lm) . j by A8, A25, A10, A22, A27, A20, A24, Def1
.= p `1 by A29, A26, Def1 ;
(M * (n,i)) `1 = p `1 by A8, A9, A10, A20, MATRIX_1:def_7;
then (X_axis (Col (M,i))) . n = p `1 by A3, A15, A12, A19, A13, Def1
.= (X_axis (Col (M,i))) . m by A4, A15, A12, A19, A30, A16, Def1 ;
hence contradiction by A3, A4, A15, A21, A12, A19, A6, SEQM_3:def_1; ::_thesis: verum
end;
theorem Th4: :: GOBOARD1:4
for M being Y_equal-in-column Y_increasing-in-line Matrix of (TOP-REAL 2)
for x being set
for n, m being Element of NAT st x in rng (Col (M,n)) & x in rng (Col (M,m)) & n in Seg (width M) & m in Seg (width M) holds
n = m
proof
let M be Y_equal-in-column Y_increasing-in-line Matrix of (TOP-REAL 2); ::_thesis: for x being set
for n, m being Element of NAT st x in rng (Col (M,n)) & x in rng (Col (M,m)) & n in Seg (width M) & m in Seg (width M) holds
n = m
assume ex x being set ex n, m being Element of NAT st
( x in rng (Col (M,n)) & x in rng (Col (M,m)) & n in Seg (width M) & m in Seg (width M) & not n = m ) ; ::_thesis: contradiction
then consider x being set , n, m being Element of NAT such that
A1: x in rng (Col (M,n)) and
A2: x in rng (Col (M,m)) and
A3: n in Seg (width M) and
A4: m in Seg (width M) and
A5: n <> m ;
reconsider Ln = Col (M,n), Lm = Col (M,m) as FinSequence of (TOP-REAL 2) ;
consider i being Nat such that
A6: i in dom Ln and
A7: Ln . i = x by A1, FINSEQ_2:10;
A8: len Ln = len M by MATRIX_1:def_8;
A9: len Lm = len M by MATRIX_1:def_8;
then A10: i in dom Lm by A6, A8, FINSEQ_3:29;
set C = Y_axis (Line (M,i));
A11: Seg (len Ln) = dom Ln by FINSEQ_1:def_3;
A12: dom M = Seg (len M) by FINSEQ_1:def_3;
then A13: Y_axis (Line (M,i)) is increasing by A6, A8, A11, Def6;
Lm . i = M * (i,m) by A6, A8, A12, A11, MATRIX_1:def_8;
then A14: Lm /. i = M * (i,m) by A10, PARTFUN1:def_6;
A15: len (Y_axis Lm) = len Lm by Def2;
consider j being Nat such that
A16: j in dom Lm and
A17: Lm . j = x by A2, FINSEQ_2:10;
A18: dom (Y_axis Lm) = Seg (len (Y_axis Lm)) by FINSEQ_1:def_3;
Ln . i = M * (i,n) by A6, A8, A12, A11, MATRIX_1:def_8;
then reconsider p = x as Point of (TOP-REAL 2) by A7;
A19: Lm /. j = p by A16, A17, PARTFUN1:def_6;
A20: Seg (len Lm) = dom Lm by FINSEQ_1:def_3;
then A21: j in dom (Y_axis Lm) by A16, A18, Def2;
Y_axis (Col (M,m)) is constant by A4, Def5;
then (Y_axis Lm) . i = (Y_axis Lm) . j by A6, A16, A18, A8, A9, A15, A11, A20, SEQM_3:def_10;
then A22: (M * (i,m)) `2 = (Y_axis Lm) . j by A6, A18, A8, A9, A15, A11, A14, Def2
.= p `2 by A21, A19, Def2 ;
A23: ( n < m or m < n ) by A5, XXREAL_0:1;
A24: ( len (Y_axis (Line (M,i))) = len (Line (M,i)) & dom (Y_axis (Line (M,i))) = Seg (len (Y_axis (Line (M,i)))) ) by Def2, FINSEQ_1:def_3;
reconsider Li = Line (M,i) as FinSequence of (TOP-REAL 2) ;
A25: (Line (M,i)) . m = M * (i,m) by A4, MATRIX_1:def_7;
A26: len (Line (M,i)) = width M by MATRIX_1:def_7;
then m in dom (Line (M,i)) by A4, FINSEQ_1:def_3;
then A27: M * (i,m) = Li /. m by A25, PARTFUN1:def_6;
A28: (Line (M,i)) . n = M * (i,n) by A3, MATRIX_1:def_7;
n in dom (Line (M,i)) by A3, A26, FINSEQ_1:def_3;
then A29: M * (i,n) = Li /. n by A28, PARTFUN1:def_6;
(M * (i,n)) `2 = p `2 by A6, A7, A8, A12, A11, MATRIX_1:def_8;
then (Y_axis (Line (M,i))) . n = p `2 by A3, A26, A24, A29, Def2
.= (Y_axis (Line (M,i))) . m by A4, A26, A24, A22, A27, Def2 ;
hence contradiction by A3, A4, A13, A26, A24, A23, SEQM_3:def_1; ::_thesis: verum
end;
begin
definition
mode Go-board is V3() X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column Matrix of (TOP-REAL 2);
end;
theorem :: GOBOARD1:5
for m, k, i, j being Element of NAT
for x being set
for G being Go-board st x = G * (m,k) & x = G * (i,j) & [m,k] in Indices G & [i,j] in Indices G holds
( m = i & k = j )
proof
let m, k, i, j be Element of NAT ; ::_thesis: for x being set
for G being Go-board st x = G * (m,k) & x = G * (i,j) & [m,k] in Indices G & [i,j] in Indices G holds
( m = i & k = j )
let x be set ; ::_thesis: for G being Go-board st x = G * (m,k) & x = G * (i,j) & [m,k] in Indices G & [i,j] in Indices G holds
( m = i & k = j )
let G be Go-board; ::_thesis: ( x = G * (m,k) & x = G * (i,j) & [m,k] in Indices G & [i,j] in Indices G implies ( m = i & k = j ) )
assume that
A1: x = G * (m,k) and
A2: x = G * (i,j) and
A3: [m,k] in Indices G and
A4: [i,j] in Indices G ; ::_thesis: ( m = i & k = j )
A5: ( len (Line (G,m)) = width G & dom (Line (G,m)) = Seg (len (Line (G,m))) ) by FINSEQ_1:def_3, MATRIX_1:def_7;
A6: Indices G = [:(dom G),(Seg (width G)):] by MATRIX_1:def_4;
then A7: k in Seg (width G) by A3, ZFMISC_1:87;
then x = (Line (G,m)) . k by A1, MATRIX_1:def_7;
then A8: x in rng (Line (G,m)) by A7, A5, FUNCT_1:def_3;
A9: ( len (Col (G,k)) = len G & dom (Col (G,k)) = Seg (len (Col (G,k))) ) by FINSEQ_1:def_3, MATRIX_1:def_8;
A10: ( len (Line (G,i)) = width G & dom (Line (G,i)) = Seg (len (Line (G,i))) ) by FINSEQ_1:def_3, MATRIX_1:def_7;
A11: ( len (Col (G,j)) = len G & dom (Col (G,j)) = Seg (len (Col (G,j))) ) by FINSEQ_1:def_3, MATRIX_1:def_8;
A12: dom G = Seg (len G) by FINSEQ_1:def_3;
A13: j in Seg (width G) by A4, A6, ZFMISC_1:87;
then x = (Line (G,i)) . j by A2, MATRIX_1:def_7;
then A14: x in rng (Line (G,i)) by A13, A10, FUNCT_1:def_3;
A15: i in dom G by A4, A6, ZFMISC_1:87;
then x = (Col (G,j)) . i by A2, MATRIX_1:def_8;
then A16: x in rng (Col (G,j)) by A15, A12, A11, FUNCT_1:def_3;
A17: m in dom G by A3, A6, ZFMISC_1:87;
then x = (Col (G,k)) . m by A1, MATRIX_1:def_8;
then x in rng (Col (G,k)) by A17, A12, A9, FUNCT_1:def_3;
hence ( m = i & k = j ) by A17, A15, A7, A13, A8, A14, A16, Th3, Th4; ::_thesis: verum
end;
theorem :: GOBOARD1:6
for f being FinSequence of (TOP-REAL 2)
for m being Element of NAT
for G being Go-board st m in dom f & f /. 1 in rng (Col (G,1)) holds
(f | m) /. 1 in rng (Col (G,1))
proof
let f be FinSequence of (TOP-REAL 2); ::_thesis: for m being Element of NAT
for G being Go-board st m in dom f & f /. 1 in rng (Col (G,1)) holds
(f | m) /. 1 in rng (Col (G,1))
let m be Element of NAT ; ::_thesis: for G being Go-board st m in dom f & f /. 1 in rng (Col (G,1)) holds
(f | m) /. 1 in rng (Col (G,1))
let G be Go-board; ::_thesis: ( m in dom f & f /. 1 in rng (Col (G,1)) implies (f | m) /. 1 in rng (Col (G,1)) )
assume that
A1: m in dom f and
A2: f /. 1 in rng (Col (G,1)) ; ::_thesis: (f | m) /. 1 in rng (Col (G,1))
1 <= m by A1, FINSEQ_3:25;
then 1 in Seg m by FINSEQ_1:1;
hence (f | m) /. 1 in rng (Col (G,1)) by A1, A2, FINSEQ_4:71; ::_thesis: verum
end;
theorem :: GOBOARD1:7
for f being FinSequence of (TOP-REAL 2)
for m being Element of NAT
for G being Go-board st m in dom f & f /. m in rng (Col (G,(width G))) holds
(f | m) /. (len (f | m)) in rng (Col (G,(width G)))
proof
let f be FinSequence of (TOP-REAL 2); ::_thesis: for m being Element of NAT
for G being Go-board st m in dom f & f /. m in rng (Col (G,(width G))) holds
(f | m) /. (len (f | m)) in rng (Col (G,(width G)))
let m be Element of NAT ; ::_thesis: for G being Go-board st m in dom f & f /. m in rng (Col (G,(width G))) holds
(f | m) /. (len (f | m)) in rng (Col (G,(width G)))
let G be Go-board; ::_thesis: ( m in dom f & f /. m in rng (Col (G,(width G))) implies (f | m) /. (len (f | m)) in rng (Col (G,(width G))) )
assume that
A1: m in dom f and
A2: f /. m in rng (Col (G,(width G))) ; ::_thesis: (f | m) /. (len (f | m)) in rng (Col (G,(width G)))
m <= len f by A1, FINSEQ_3:25;
then A3: len (f | m) = m by FINSEQ_1:59;
1 <= m by A1, FINSEQ_3:25;
then m in Seg m by FINSEQ_1:1;
hence (f | m) /. (len (f | m)) in rng (Col (G,(width G))) by A1, A2, A3, FINSEQ_4:71; ::_thesis: verum
end;
theorem Th8: :: GOBOARD1:8
for f being FinSequence of (TOP-REAL 2)
for i, n, m, k being Element of NAT
for G being Go-board st rng f misses rng (Col (G,i)) & f /. n = G * (m,k) & n in dom f & m in dom G holds
i <> k
proof
let f be FinSequence of (TOP-REAL 2); ::_thesis: for i, n, m, k being Element of NAT
for G being Go-board st rng f misses rng (Col (G,i)) & f /. n = G * (m,k) & n in dom f & m in dom G holds
i <> k
let i, n, m, k be Element of NAT ; ::_thesis: for G being Go-board st rng f misses rng (Col (G,i)) & f /. n = G * (m,k) & n in dom f & m in dom G holds
i <> k
let G be Go-board; ::_thesis: ( rng f misses rng (Col (G,i)) & f /. n = G * (m,k) & n in dom f & m in dom G implies i <> k )
assume that
A1: (rng f) /\ (rng (Col (G,i))) = {} and
A2: f /. n = G * (m,k) and
A3: n in dom f and
A4: m in dom G and
A5: i = k ; :: according to XBOOLE_0:def_7 ::_thesis: contradiction
f . n = G * (m,k) by A2, A3, PARTFUN1:def_6;
then A6: G * (m,i) in rng f by A3, A5, FUNCT_1:def_3;
A7: ( dom G = Seg (len G) & dom (Col (G,i)) = Seg (len (Col (G,i))) ) by FINSEQ_1:def_3;
( len (Col (G,i)) = len G & (Col (G,i)) . m = G * (m,i) ) by A4, MATRIX_1:def_8;
then G * (m,i) in rng (Col (G,i)) by A4, A7, FUNCT_1:def_3;
hence contradiction by A1, A6, XBOOLE_0:def_4; ::_thesis: verum
end;
definition
let G be Go-board;
let i be Element of NAT ;
assume A1: ( i in Seg (width G) & width G > 1 ) ;
func DelCol (G,i) -> Go-board means :Def8: :: GOBOARD1:def 8
( len it = len G & ( for k being Element of NAT st k in dom G holds
it . k = Del ((Line (G,k)),i) ) );
existence
ex b1 being Go-board st
( len b1 = len G & ( for k being Element of NAT st k in dom G holds
b1 . k = Del ((Line (G,k)),i) ) )
proof
defpred S1[ Nat, Nat, Point of (TOP-REAL 2)] means $3 = (Del ((Line (G,$1)),i)) . $2;
A2: ( 0 < len G & 0 < width G ) by Lm1;
then consider m being Nat such that
A3: width G = m + 1 by NAT_1:6;
reconsider m = m as Element of NAT by ORDINAL1:def_12;
A4: Seg (len G) = dom G by FINSEQ_1:def_3;
A5: for k being Element of NAT st k in dom G holds
len (Del ((Line (G,k)),i)) = m
proof
let k be Element of NAT ; ::_thesis: ( k in dom G implies len (Del ((Line (G,k)),i)) = m )
assume k in dom G ; ::_thesis: len (Del ((Line (G,k)),i)) = m
A6: len (Line (G,k)) = width G by MATRIX_1:def_7;
then i in dom (Line (G,k)) by A1, FINSEQ_1:def_3;
then ex j being Nat st
( len (Line (G,k)) = j + 1 & len (Del ((Line (G,k)),i)) = j ) by FINSEQ_3:104;
hence len (Del ((Line (G,k)),i)) = m by A3, A6; ::_thesis: verum
end;
A7: for k, j being Nat st [k,j] in [:(Seg (len G)),(Seg m):] holds
ex x being Point of (TOP-REAL 2) st S1[k,j,x]
proof
let k, j be Nat; ::_thesis: ( [k,j] in [:(Seg (len G)),(Seg m):] implies ex x being Point of (TOP-REAL 2) st S1[k,j,x] )
assume [k,j] in [:(Seg (len G)),(Seg m):] ; ::_thesis: ex x being Point of (TOP-REAL 2) st S1[k,j,x]
then A8: ( k in dom G & j in Seg m ) by A4, ZFMISC_1:87;
reconsider p = Del ((Line (G,k)),i) as FinSequence of (TOP-REAL 2) by FINSEQ_3:105;
len p = m by A5, A8;
then j in dom p by A8, FINSEQ_1:def_3;
then reconsider x = p . j as Point of (TOP-REAL 2) by FINSEQ_2:11;
take x ; ::_thesis: S1[k,j,x]
thus S1[k,j,x] ; ::_thesis: verum
end;
consider N being Matrix of len G,m, the carrier of (TOP-REAL 2) such that
A9: for k, j being Nat st [k,j] in Indices N holds
S1[k,j,N * (k,j)] from MATRIX_1:sch_2(A7);
A10: Seg (len N) = dom N by FINSEQ_1:def_3;
A11: ( len N = len G & width N = m & Indices N = [:(dom G),(Seg m):] ) by A2, A4, MATRIX_1:23;
A12: for k, j being Element of NAT st k in dom G & j in Seg m holds
N * (k,j) = (Del ((Line (G,k)),i)) . j
proof
let k, j be Element of NAT ; ::_thesis: ( k in dom G & j in Seg m implies N * (k,j) = (Del ((Line (G,k)),i)) . j )
assume ( k in dom G & j in Seg m ) ; ::_thesis: N * (k,j) = (Del ((Line (G,k)),i)) . j
then [k,j] in Indices N by A11, ZFMISC_1:87;
hence N * (k,j) = (Del ((Line (G,k)),i)) . j by A9; ::_thesis: verum
end;
A13: for k, j being Element of NAT st k in dom G & j in Seg m & not N * (k,j) = (Line (G,k)) . j holds
N * (k,j) = (Line (G,k)) . (j + 1)
proof
let k, j be Element of NAT ; ::_thesis: ( k in dom G & j in Seg m & not N * (k,j) = (Line (G,k)) . j implies N * (k,j) = (Line (G,k)) . (j + 1) )
assume A14: ( k in dom G & j in Seg m ) ; ::_thesis: ( N * (k,j) = (Line (G,k)) . j or N * (k,j) = (Line (G,k)) . (j + 1) )
then A15: N * (k,j) = (Del ((Line (G,k)),i)) . j by A12;
A16: len (Line (G,k)) = m + 1 by A3, MATRIX_1:def_7;
i in Seg (len (Line (G,k))) by A1, MATRIX_1:def_7;
then i in dom (Line (G,k)) by FINSEQ_1:def_3;
hence ( N * (k,j) = (Line (G,k)) . j or N * (k,j) = (Line (G,k)) . (j + 1) ) by A14, A15, A16, SEQM_3:44; ::_thesis: verum
end;
A17: for k being Element of NAT holds
( not k in Seg m or Col (N,k) = Col (G,k) or Col (N,k) = Col (G,(k + 1)) )
proof
let k be Element of NAT ; ::_thesis: ( not k in Seg m or Col (N,k) = Col (G,k) or Col (N,k) = Col (G,(k + 1)) )
assume A18: k in Seg m ; ::_thesis: ( Col (N,k) = Col (G,k) or Col (N,k) = Col (G,(k + 1)) )
then A19: ( 1 <= k & k <= m ) by FINSEQ_1:1;
( m <= m + 1 & k <= k + 1 ) by NAT_1:11;
then ( k <= m + 1 & 1 <= k + 1 & k + 1 <= m + 1 ) by A19, XREAL_1:6, XXREAL_0:2;
then A20: ( k in Seg (width G) & k + 1 in Seg (width G) ) by A3, A19, FINSEQ_1:1;
A21: ( len (Col (N,k)) = len N & len (Col (G,k)) = len G & len (Col (G,(k + 1))) = len G ) by MATRIX_1:def_8;
now__::_thesis:_(_Col_(N,k)_=_Col_(G,k)_or_Col_(N,k)_=_Col_(G,(k_+_1))_)
percases ( k < i or k >= i ) ;
supposeA22: k < i ; ::_thesis: ( Col (N,k) = Col (G,k) or Col (N,k) = Col (G,(k + 1)) )
now__::_thesis:_for_j_being_Nat_st_1_<=_j_&_j_<=_len_(Col_(N,k))_holds_
(Col_(N,k))_._j_=_(Col_(G,k))_._j
let j be Nat; ::_thesis: ( 1 <= j & j <= len (Col (N,k)) implies (Col (N,k)) . j = (Col (G,k)) . j )
assume ( 1 <= j & j <= len (Col (N,k)) ) ; ::_thesis: (Col (N,k)) . j = (Col (G,k)) . j
then A23: j in dom N by A21, FINSEQ_3:25;
hence (Col (N,k)) . j = N * (j,k) by MATRIX_1:def_8
.= (Del ((Line (G,j)),i)) . k by A4, A10, A11, A12, A18, A23
.= (Line (G,j)) . k by A22, FINSEQ_3:110
.= (Col (G,k)) . j by A4, A10, A11, A20, A23, Th2 ;
::_thesis: verum
end;
hence ( Col (N,k) = Col (G,k) or Col (N,k) = Col (G,(k + 1)) ) by A11, A21, FINSEQ_1:14; ::_thesis: verum
end;
supposeA24: k >= i ; ::_thesis: ( Col (N,k) = Col (G,k) or Col (N,k) = Col (G,(k + 1)) )
now__::_thesis:_for_j_being_Nat_st_1_<=_j_&_j_<=_len_(Col_(N,k))_holds_
(Col_(N,k))_._j_=_(Col_(G,(k_+_1)))_._j
let j be Nat; ::_thesis: ( 1 <= j & j <= len (Col (N,k)) implies (Col (N,k)) . j = (Col (G,(k + 1))) . j )
assume ( 1 <= j & j <= len (Col (N,k)) ) ; ::_thesis: (Col (N,k)) . j = (Col (G,(k + 1))) . j
then A25: j in dom N by A21, FINSEQ_3:25;
A26: len (Line (G,j)) = m + 1 by A3, MATRIX_1:def_7;
A27: dom (Line (G,j)) = Seg (len (Line (G,j))) by FINSEQ_1:def_3;
thus (Col (N,k)) . j = N * (j,k) by A25, MATRIX_1:def_8
.= (Del ((Line (G,j)),i)) . k by A4, A10, A11, A12, A18, A25
.= (Line (G,j)) . (k + 1) by A1, A3, A19, A24, A26, A27, FINSEQ_3:111
.= (Col (G,(k + 1))) . j by A4, A10, A11, A20, A25, Th2 ; ::_thesis: verum
end;
hence ( Col (N,k) = Col (G,k) or Col (N,k) = Col (G,(k + 1)) ) by A11, A21, FINSEQ_1:14; ::_thesis: verum
end;
end;
end;
hence ( Col (N,k) = Col (G,k) or Col (N,k) = Col (G,(k + 1)) ) ; ::_thesis: verum
end;
reconsider M = N as Matrix of (TOP-REAL 2) ;
1 - 1 < m by A1, A3, XREAL_1:19;
then A28: ( 0 < len M & 0 < width M ) by A2, MATRIX_1:23;
A29: now__::_thesis:_for_k_being_Element_of_NAT_st_k_in_dom_M_holds_
X_axis_(Line_(M,k))_is_constant
let k be Element of NAT ; ::_thesis: ( k in dom M implies X_axis (Line (M,k)) is constant )
assume A30: k in dom M ; ::_thesis: X_axis (Line (M,k)) is constant
then A31: X_axis (Line (G,k)) is constant by A4, A10, A11, Def4;
m <= m + 1 by NAT_1:11;
then A32: Seg m c= Seg (width G) by A3, FINSEQ_1:5;
reconsider L = Line (M,k), lg = Line (G,k) as FinSequence of (TOP-REAL 2) ;
set X = X_axis L;
set xg = X_axis lg;
now__::_thesis:_for_n,_j_being_Element_of_NAT_st_n_in_dom_(X_axis_L)_&_j_in_dom_(X_axis_L)_holds_
(X_axis_L)_._n_=_(X_axis_L)_._j
let n, j be Element of NAT ; ::_thesis: ( n in dom (X_axis L) & j in dom (X_axis L) implies (X_axis L) . n = (X_axis L) . j )
assume A33: ( n in dom (X_axis L) & j in dom (X_axis L) ) ; ::_thesis: (X_axis L) . n = (X_axis L) . j
A34: ( dom (X_axis L) = Seg (len (X_axis L)) & len (X_axis L) = len L & len L = width M & dom (X_axis lg) = Seg (len (X_axis lg)) & len (X_axis lg) = len lg & len lg = width G ) by Def1, FINSEQ_1:def_3, MATRIX_1:def_7;
then A35: ( L . n = M * (k,n) & L . j = M * (k,j) & n in Seg m & j in Seg m ) by A2, A33, MATRIX_1:23, MATRIX_1:def_7;
then A36: ( ( L . n = lg . n or L . n = lg . (n + 1) ) & ( L . j = lg . j or L . j = lg . (j + 1) ) ) by A4, A10, A11, A13, A30;
( n in dom L & j in dom L ) by A33, A34, FINSEQ_1:def_3;
then ( L . n = L /. n & L . j = L /. j ) by PARTFUN1:def_6;
then A37: ( (X_axis L) . n = (M * (k,n)) `1 & (X_axis L) . j = (M * (k,j)) `1 ) by A33, A35, Def1;
( 1 <= n & n <= m & 1 <= j & j <= m ) by A11, A33, A34, FINSEQ_3:25;
then A38: ( n <= n + 1 & n + 1 <= m + 1 & j <= j + 1 & j + 1 <= m + 1 ) by NAT_1:11, XREAL_1:6;
( 1 <= n + 1 & 1 <= j + 1 ) by NAT_1:11;
then A39: ( n + 1 in Seg (width G) & j + 1 in Seg (width G) & n in Seg (width G) & j in Seg (width G) ) by A3, A11, A32, A33, A34, A38, FINSEQ_3:25;
then A40: ( lg . n = G * (k,n) & lg . (n + 1) = G * (k,(n + 1)) & lg . j = G * (k,j) & lg . (j + 1) = G * (k,(j + 1)) ) by MATRIX_1:def_7;
dom lg = Seg (len (X_axis lg)) by A34, FINSEQ_1:def_3;
then ( lg . n = lg /. n & lg . (n + 1) = lg /. (n + 1) & lg . j = lg /. j & lg . (j + 1) = lg /. (j + 1) ) by A34, A39, PARTFUN1:def_6;
then ( (X_axis lg) . n = (G * (k,n)) `1 & (X_axis lg) . (n + 1) = (G * (k,(n + 1))) `1 & (X_axis lg) . j = (G * (k,j)) `1 & (X_axis lg) . (j + 1) = (G * (k,(j + 1))) `1 ) by A34, A39, A40, Def1;
hence (X_axis L) . n = (X_axis L) . j by A31, A34, A35, A36, A37, A39, A40, SEQM_3:def_10; ::_thesis: verum
end;
hence X_axis (Line (M,k)) is constant by SEQM_3:def_10; ::_thesis: verum
end;
A41: now__::_thesis:_for_k_being_Element_of_NAT_st_k_in_Seg_(width_M)_holds_
Y_axis_(Col_(M,k))_is_constant
let k be Element of NAT ; ::_thesis: ( k in Seg (width M) implies Y_axis (Col (M,k)) is constant )
assume A42: k in Seg (width M) ; ::_thesis: Y_axis (Col (M,k)) is constant
then A43: ( Col (M,k) = Col (G,k) or Col (M,k) = Col (G,(k + 1)) ) by A11, A17;
A44: ( 1 <= k & k <= m ) by A11, A42, FINSEQ_1:1;
( m <= m + 1 & k <= k + 1 ) by NAT_1:11;
then ( k <= m + 1 & 1 <= k + 1 & k + 1 <= m + 1 ) by A44, XREAL_1:6, XXREAL_0:2;
then ( k in Seg (width G) & k + 1 in Seg (width G) ) by A3, A44, FINSEQ_1:1;
hence Y_axis (Col (M,k)) is constant by A43, Def5; ::_thesis: verum
end;
A45: now__::_thesis:_for_k_being_Element_of_NAT_st_k_in_dom_M_holds_
Y_axis_(Line_(M,k))_is_increasing
let k be Element of NAT ; ::_thesis: ( k in dom M implies Y_axis (Line (M,k)) is increasing )
reconsider L = Line (M,k), lg = Line (G,k) as FinSequence of (TOP-REAL 2) ;
set X = Y_axis L;
set xg = Y_axis lg;
m <= m + 1 by NAT_1:11;
then A46: Seg m c= Seg (width G) by A3, FINSEQ_1:5;
assume A47: k in dom M ; ::_thesis: Y_axis (Line (M,k)) is increasing
then A48: Y_axis lg is increasing by A4, A10, A11, Def6;
now__::_thesis:_for_n,_j_being_Element_of_NAT_st_n_in_dom_(Y_axis_L)_&_j_in_dom_(Y_axis_L)_&_n_<_j_holds_
(Y_axis_L)_._n_<_(Y_axis_L)_._j
let n, j be Element of NAT ; ::_thesis: ( n in dom (Y_axis L) & j in dom (Y_axis L) & n < j implies (Y_axis L) . b1 < (Y_axis L) . b2 )
assume A49: ( n in dom (Y_axis L) & j in dom (Y_axis L) & n < j ) ; ::_thesis: (Y_axis L) . b1 < (Y_axis L) . b2
A50: ( dom (Y_axis L) = Seg (len (Y_axis L)) & len (Y_axis L) = len L & len L = width M & dom (Y_axis lg) = Seg (len (Y_axis lg)) & len (Y_axis lg) = len lg & len lg = width G ) by Def2, FINSEQ_1:def_3, MATRIX_1:def_7;
then A51: ( L . n = M * (k,n) & L . j = M * (k,j) & n in Seg m & j in Seg m ) by A2, A49, MATRIX_1:23, MATRIX_1:def_7;
dom L = Seg (len (Y_axis L)) by A50, FINSEQ_1:def_3;
then ( L . n = L /. n & L . j = L /. j ) by A49, A50, PARTFUN1:def_6;
then A52: ( (Y_axis L) . n = (M * (k,n)) `2 & (Y_axis L) . j = (M * (k,j)) `2 ) by A49, A51, Def2;
A53: ( 1 <= n & n <= m & 1 <= j & j <= m ) by A11, A49, A50, FINSEQ_3:25;
then A54: ( n <= n + 1 & n + 1 <= m + 1 & j <= j + 1 & j + 1 <= m + 1 ) by NAT_1:11, XREAL_1:6;
( 1 <= n + 1 & 1 <= j + 1 ) by NAT_1:11;
then A55: ( n + 1 in Seg (width G) & j + 1 in Seg (width G) & n in Seg (width G) & j in Seg (width G) ) by A3, A11, A46, A49, A50, A54, FINSEQ_3:25;
then A56: ( lg . n = G * (k,n) & lg . (n + 1) = G * (k,(n + 1)) & lg . j = G * (k,j) & lg . (j + 1) = G * (k,(j + 1)) ) by MATRIX_1:def_7;
dom lg = Seg (len (Y_axis lg)) by A50, FINSEQ_1:def_3;
then ( lg . n = lg /. n & lg . (n + 1) = lg /. (n + 1) & lg . j = lg /. j & lg . (j + 1) = lg /. (j + 1) ) by A50, A55, PARTFUN1:def_6;
then A57: ( (Y_axis lg) . n = (G * (k,n)) `2 & (Y_axis lg) . (n + 1) = (G * (k,(n + 1))) `2 & (Y_axis lg) . j = (G * (k,j)) `2 & (Y_axis lg) . (j + 1) = (G * (k,(j + 1))) `2 ) by A50, A55, A56, Def2;
set r = (Y_axis L) . n;
set s = (Y_axis L) . j;
A58: dom lg = Seg (len lg) by FINSEQ_1:def_3;
percases ( j < i or j >= i ) ;
supposeA59: j < i ; ::_thesis: (Y_axis L) . b1 < (Y_axis L) . b2
then A60: n < i by A49, XXREAL_0:2;
A61: M * (k,n) = (Del (lg,i)) . n by A4, A10, A11, A12, A47, A49, A50
.= G * (k,n) by A56, A60, FINSEQ_3:110 ;
M * (k,j) = (Del (lg,i)) . j by A4, A10, A11, A12, A47, A49, A50
.= G * (k,j) by A56, A59, FINSEQ_3:110 ;
hence (Y_axis L) . n < (Y_axis L) . j by A11, A46, A48, A49, A50, A52, A57, A61, SEQM_3:def_1; ::_thesis: verum
end;
supposeA62: j >= i ; ::_thesis: (Y_axis L) . b1 < (Y_axis L) . b2
A63: M * (k,j) = (Del (lg,i)) . j by A4, A10, A11, A12, A47, A49, A50
.= G * (k,(j + 1)) by A1, A3, A50, A53, A56, A58, A62, FINSEQ_3:111 ;
now__::_thesis:_(Y_axis_L)_._n_<_(Y_axis_L)_._j
percases ( n < i or n >= i ) ;
supposeA64: n < i ; ::_thesis: (Y_axis L) . n < (Y_axis L) . j
j <= j + 1 by NAT_1:11;
then A65: n < j + 1 by A49, XXREAL_0:2;
M * (k,n) = (Del (lg,i)) . n by A4, A10, A11, A12, A47, A49, A50
.= G * (k,n) by A56, A64, FINSEQ_3:110 ;
hence (Y_axis L) . n < (Y_axis L) . j by A48, A50, A52, A55, A57, A63, A65, SEQM_3:def_1; ::_thesis: verum
end;
supposeA66: n >= i ; ::_thesis: (Y_axis L) . n < (Y_axis L) . j
A67: n + 1 < j + 1 by A49, XREAL_1:6;
M * (k,n) = (Del (lg,i)) . n by A4, A10, A11, A12, A47, A49, A50
.= G * (k,(n + 1)) by A1, A3, A50, A53, A56, A58, A66, FINSEQ_3:111 ;
hence (Y_axis L) . n < (Y_axis L) . j by A48, A50, A52, A55, A57, A63, A67, SEQM_3:def_1; ::_thesis: verum
end;
end;
end;
hence (Y_axis L) . n < (Y_axis L) . j ; ::_thesis: verum
end;
end;
end;
hence Y_axis (Line (M,k)) is increasing by SEQM_3:def_1; ::_thesis: verum
end;
now__::_thesis:_for_k_being_Element_of_NAT_st_k_in_Seg_(width_M)_holds_
X_axis_(Col_(M,k))_is_increasing
let k be Element of NAT ; ::_thesis: ( k in Seg (width M) implies X_axis (Col (M,k)) is increasing )
assume A68: k in Seg (width M) ; ::_thesis: X_axis (Col (M,k)) is increasing
then A69: ( Col (M,k) = Col (G,k) or Col (M,k) = Col (G,(k + 1)) ) by A11, A17;
A70: ( 1 <= k & k <= m ) by A11, A68, FINSEQ_1:1;
( m <= m + 1 & k <= k + 1 ) by NAT_1:11;
then ( k <= m + 1 & 1 <= k + 1 & k + 1 <= m + 1 ) by A70, XREAL_1:6, XXREAL_0:2;
then ( k in Seg (width G) & k + 1 in Seg (width G) ) by A3, A70, FINSEQ_1:1;
hence X_axis (Col (M,k)) is increasing by A69, Def7; ::_thesis: verum
end;
then reconsider M = M as V3() X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column Matrix of (TOP-REAL 2) by A28, A29, A41, A45, Def3, Def4, Def5, Def6, Def7;
take M ; ::_thesis: ( len M = len G & ( for k being Element of NAT st k in dom G holds
M . k = Del ((Line (G,k)),i) ) )
thus A71: len M = len G by A2, MATRIX_1:23; ::_thesis: for k being Element of NAT st k in dom G holds
M . k = Del ((Line (G,k)),i)
let k be Element of NAT ; ::_thesis: ( k in dom G implies M . k = Del ((Line (G,k)),i) )
assume A72: k in dom G ; ::_thesis: M . k = Del ((Line (G,k)),i)
then A73: M . k = Line (M,k) by A4, A10, A71, MATRIX_2:16;
then reconsider s = M . k as FinSequence ;
A74: len s = m by A11, A73, MATRIX_1:def_7;
A75: len (Del ((Line (G,k)),i)) = m by A5, A72;
A76: dom s = Seg m by A74, FINSEQ_1:def_3;
now__::_thesis:_for_j_being_Nat_st_j_in_dom_s_holds_
s_._j_=_(Del_((Line_(G,k)),i))_._j
let j be Nat; ::_thesis: ( j in dom s implies s . j = (Del ((Line (G,k)),i)) . j )
assume A77: j in dom s ; ::_thesis: s . j = (Del ((Line (G,k)),i)) . j
then (Line (M,k)) . j = M * (k,j) by A11, A76, MATRIX_1:def_7;
hence s . j = (Del ((Line (G,k)),i)) . j by A12, A72, A73, A77, A76; ::_thesis: verum
end;
hence M . k = Del ((Line (G,k)),i) by A74, A75, FINSEQ_2:9; ::_thesis: verum
end;
uniqueness
for b1, b2 being Go-board st len b1 = len G & ( for k being Element of NAT st k in dom G holds
b1 . k = Del ((Line (G,k)),i) ) & len b2 = len G & ( for k being Element of NAT st k in dom G holds
b2 . k = Del ((Line (G,k)),i) ) holds
b1 = b2
proof
let G1, G2 be Go-board; ::_thesis: ( len G1 = len G & ( for k being Element of NAT st k in dom G holds
G1 . k = Del ((Line (G,k)),i) ) & len G2 = len G & ( for k being Element of NAT st k in dom G holds
G2 . k = Del ((Line (G,k)),i) ) implies G1 = G2 )
assume that
A78: ( len G1 = len G & ( for k being Element of NAT st k in dom G holds
G1 . k = Del ((Line (G,k)),i) ) ) and
A79: ( len G2 = len G & ( for k being Element of NAT st k in dom G holds
G2 . k = Del ((Line (G,k)),i) ) ) ; ::_thesis: G1 = G2
A80: dom G1 = Seg (len G) by A78, FINSEQ_1:def_3;
now__::_thesis:_for_k_being_Nat_st_k_in_dom_G1_holds_
G1_._k_=_G2_._k
let k be Nat; ::_thesis: ( k in dom G1 implies G1 . k = G2 . k )
assume k in dom G1 ; ::_thesis: G1 . k = G2 . k
then A81: k in dom G by A80, FINSEQ_1:def_3;
hence G1 . k = Del ((Line (G,k)),i) by A78
.= G2 . k by A79, A81 ;
::_thesis: verum
end;
hence G1 = G2 by A78, A79, FINSEQ_2:9; ::_thesis: verum
end;
end;
:: deftheorem Def8 defines DelCol GOBOARD1:def_8_:_
for G being Go-board
for i being Element of NAT st i in Seg (width G) & width G > 1 holds
for b3 being Go-board holds
( b3 = DelCol (G,i) iff ( len b3 = len G & ( for k being Element of NAT st k in dom G holds
b3 . k = Del ((Line (G,k)),i) ) ) );
theorem Th9: :: GOBOARD1:9
for i, k being Element of NAT
for G being Go-board st i in Seg (width G) & width G > 1 & k in dom G holds
Line ((DelCol (G,i)),k) = Del ((Line (G,k)),i)
proof
let i, k be Element of NAT ; ::_thesis: for G being Go-board st i in Seg (width G) & width G > 1 & k in dom G holds
Line ((DelCol (G,i)),k) = Del ((Line (G,k)),i)
let G be Go-board; ::_thesis: ( i in Seg (width G) & width G > 1 & k in dom G implies Line ((DelCol (G,i)),k) = Del ((Line (G,k)),i) )
set D = DelCol (G,i);
assume that
A1: ( i in Seg (width G) & width G > 1 ) and
A2: k in dom G ; ::_thesis: Line ((DelCol (G,i)),k) = Del ((Line (G,k)),i)
len (DelCol (G,i)) = len G by A1, Def8;
then A3: dom (DelCol (G,i)) = dom G by FINSEQ_3:29;
(DelCol (G,i)) . k = Del ((Line (G,k)),i) by A1, A2, Def8;
hence Line ((DelCol (G,i)),k) = Del ((Line (G,k)),i) by A2, A3, MATRIX_2:16; ::_thesis: verum
end;
theorem Th10: :: GOBOARD1:10
for i, m being Element of NAT
for G being Go-board st i in Seg (width G) & width G = m + 1 & m > 0 holds
width (DelCol (G,i)) = m
proof
let i, m be Element of NAT ; ::_thesis: for G being Go-board st i in Seg (width G) & width G = m + 1 & m > 0 holds
width (DelCol (G,i)) = m
let G be Go-board; ::_thesis: ( i in Seg (width G) & width G = m + 1 & m > 0 implies width (DelCol (G,i)) = m )
set D = DelCol (G,i);
assume that
A1: i in Seg (width G) and
A2: width G = m + 1 and
A3: m > 0 ; ::_thesis: width (DelCol (G,i)) = m
0 < len G by Lm1;
then 0 + 1 <= len G by NAT_1:13;
then A4: 1 in dom G by FINSEQ_3:25;
0 + 1 < width G by A2, A3, XREAL_1:6;
then A5: Line ((DelCol (G,i)),1) = Del ((Line (G,1)),i) by A1, A4, Th9;
A6: ( dom (Line (G,1)) = Seg (len (Line (G,1))) & len (Line ((DelCol (G,i)),1)) = width (DelCol (G,i)) ) by FINSEQ_1:def_3, MATRIX_1:def_7;
len (Line (G,1)) = m + 1 by A2, MATRIX_1:def_7;
hence width (DelCol (G,i)) = m by A1, A2, A5, A6, FINSEQ_3:109; ::_thesis: verum
end;
theorem :: GOBOARD1:11
for i being Element of NAT
for G being Go-board st i in Seg (width G) & width G > 1 holds
width G = (width (DelCol (G,i))) + 1
proof
let i be Element of NAT ; ::_thesis: for G being Go-board st i in Seg (width G) & width G > 1 holds
width G = (width (DelCol (G,i))) + 1
let G be Go-board; ::_thesis: ( i in Seg (width G) & width G > 1 implies width G = (width (DelCol (G,i))) + 1 )
assume that
A1: i in Seg (width G) and
A2: width G > 1 ; ::_thesis: width G = (width (DelCol (G,i))) + 1
ex m being Element of NAT st
( width G = m + 1 & m > 0 ) by A2, SEQM_3:43;
hence width G = (width (DelCol (G,i))) + 1 by A1, Th10; ::_thesis: verum
end;
theorem Th12: :: GOBOARD1:12
for i, n, m being Element of NAT
for G being Go-board st i in Seg (width G) & width G > 1 & n in dom G & m in Seg (width (DelCol (G,i))) holds
(DelCol (G,i)) * (n,m) = (Del ((Line (G,n)),i)) . m
proof
let i, n, m be Element of NAT ; ::_thesis: for G being Go-board st i in Seg (width G) & width G > 1 & n in dom G & m in Seg (width (DelCol (G,i))) holds
(DelCol (G,i)) * (n,m) = (Del ((Line (G,n)),i)) . m
let G be Go-board; ::_thesis: ( i in Seg (width G) & width G > 1 & n in dom G & m in Seg (width (DelCol (G,i))) implies (DelCol (G,i)) * (n,m) = (Del ((Line (G,n)),i)) . m )
assume that
A1: ( i in Seg (width G) & width G > 1 & n in dom G ) and
A2: m in Seg (width (DelCol (G,i))) ; ::_thesis: (DelCol (G,i)) * (n,m) = (Del ((Line (G,n)),i)) . m
thus (DelCol (G,i)) * (n,m) = (Line ((DelCol (G,i)),n)) . m by A2, MATRIX_1:def_7
.= (Del ((Line (G,n)),i)) . m by A1, Th9 ; ::_thesis: verum
end;
theorem Th13: :: GOBOARD1:13
for i, m, k being Element of NAT
for G being Go-board st i in Seg (width G) & width G = m + 1 & m > 0 & 1 <= k & k < i holds
( Col ((DelCol (G,i)),k) = Col (G,k) & k in Seg (width (DelCol (G,i))) & k in Seg (width G) )
proof
let i, m, k be Element of NAT ; ::_thesis: for G being Go-board st i in Seg (width G) & width G = m + 1 & m > 0 & 1 <= k & k < i holds
( Col ((DelCol (G,i)),k) = Col (G,k) & k in Seg (width (DelCol (G,i))) & k in Seg (width G) )
let G be Go-board; ::_thesis: ( i in Seg (width G) & width G = m + 1 & m > 0 & 1 <= k & k < i implies ( Col ((DelCol (G,i)),k) = Col (G,k) & k in Seg (width (DelCol (G,i))) & k in Seg (width G) ) )
set N = DelCol (G,i);
assume that
A1: i in Seg (width G) and
A2: width G = m + 1 and
A3: m > 0 and
A4: 1 <= k and
A5: k < i ; ::_thesis: ( Col ((DelCol (G,i)),k) = Col (G,k) & k in Seg (width (DelCol (G,i))) & k in Seg (width G) )
A6: width (DelCol (G,i)) = m by A1, A2, A3, Th10;
A7: 1 < width G by A2, A3, SEQM_3:43;
then A8: len (DelCol (G,i)) = len G by A1, Def8;
i <= m + 1 by A1, A2, FINSEQ_1:1;
then A9: k < m + 1 by A5, XXREAL_0:2;
then A10: k in Seg (width G) by A2, A4, FINSEQ_1:1;
A11: len (Col (G,k)) = len G by MATRIX_1:def_8;
A12: len (Col ((DelCol (G,i)),k)) = len (DelCol (G,i)) by MATRIX_1:def_8;
A13: k <= m by A9, NAT_1:13;
then A14: k in Seg (width (DelCol (G,i))) by A4, A6, FINSEQ_1:1;
now__::_thesis:_for_j_being_Nat_st_1_<=_j_&_j_<=_len_(Col_((DelCol_(G,i)),k))_holds_
(Col_((DelCol_(G,i)),k))_._j_=_(Col_(G,k))_._j
let j be Nat; ::_thesis: ( 1 <= j & j <= len (Col ((DelCol (G,i)),k)) implies (Col ((DelCol (G,i)),k)) . j = (Col (G,k)) . j )
A15: ( dom (DelCol (G,i)) = Seg (len (DelCol (G,i))) & dom G = Seg (len G) ) by FINSEQ_1:def_3;
assume ( 1 <= j & j <= len (Col ((DelCol (G,i)),k)) ) ; ::_thesis: (Col ((DelCol (G,i)),k)) . j = (Col (G,k)) . j
then A16: j in dom (DelCol (G,i)) by A12, FINSEQ_3:25;
hence (Col ((DelCol (G,i)),k)) . j = (DelCol (G,i)) * (j,k) by MATRIX_1:def_8
.= (Del ((Line (G,j)),i)) . k by A1, A14, A7, A8, A16, A15, Th12
.= (Line (G,j)) . k by A5, FINSEQ_3:110
.= (Col (G,k)) . j by A10, A8, A16, A15, Th2 ;
::_thesis: verum
end;
hence ( Col ((DelCol (G,i)),k) = Col (G,k) & k in Seg (width (DelCol (G,i))) & k in Seg (width G) ) by A2, A4, A6, A9, A13, A12, A11, A8, FINSEQ_1:1, FINSEQ_1:14; ::_thesis: verum
end;
theorem Th14: :: GOBOARD1:14
for i, m, k being Element of NAT
for G being Go-board st i in Seg (width G) & width G = m + 1 & m > 0 & i <= k & k <= m holds
( Col ((DelCol (G,i)),k) = Col (G,(k + 1)) & k in Seg (width (DelCol (G,i))) & k + 1 in Seg (width G) )
proof
let i, m, k be Element of NAT ; ::_thesis: for G being Go-board st i in Seg (width G) & width G = m + 1 & m > 0 & i <= k & k <= m holds
( Col ((DelCol (G,i)),k) = Col (G,(k + 1)) & k in Seg (width (DelCol (G,i))) & k + 1 in Seg (width G) )
let G be Go-board; ::_thesis: ( i in Seg (width G) & width G = m + 1 & m > 0 & i <= k & k <= m implies ( Col ((DelCol (G,i)),k) = Col (G,(k + 1)) & k in Seg (width (DelCol (G,i))) & k + 1 in Seg (width G) ) )
set N = DelCol (G,i);
assume that
A1: i in Seg (width G) and
A2: width G = m + 1 and
A3: m > 0 and
A4: i <= k and
A5: k <= m ; ::_thesis: ( Col ((DelCol (G,i)),k) = Col (G,(k + 1)) & k in Seg (width (DelCol (G,i))) & k + 1 in Seg (width G) )
A6: len (Col ((DelCol (G,i)),k)) = len (DelCol (G,i)) by MATRIX_1:def_8;
A7: 1 < width G by A2, A3, SEQM_3:43;
then A8: len (DelCol (G,i)) = len G by A1, Def8;
A9: ( 1 <= k + 1 & k + 1 <= m + 1 ) by A5, NAT_1:11, XREAL_1:6;
then A10: k + 1 in Seg (width G) by A2, FINSEQ_1:1;
1 <= i by A1, FINSEQ_1:1;
then A11: 1 <= k by A4, XXREAL_0:2;
A12: len (Col (G,(k + 1))) = len G by MATRIX_1:def_8;
A13: width (DelCol (G,i)) = m by A1, A2, A3, Th10;
then A14: k in Seg (width (DelCol (G,i))) by A5, A11, FINSEQ_1:1;
now__::_thesis:_for_j_being_Nat_st_1_<=_j_&_j_<=_len_(Col_((DelCol_(G,i)),k))_holds_
(Col_((DelCol_(G,i)),k))_._j_=_(Col_(G,(k_+_1)))_._j
let j be Nat; ::_thesis: ( 1 <= j & j <= len (Col ((DelCol (G,i)),k)) implies (Col ((DelCol (G,i)),k)) . j = (Col (G,(k + 1))) . j )
A15: ( dom (DelCol (G,i)) = Seg (len (DelCol (G,i))) & dom G = Seg (len G) ) by FINSEQ_1:def_3;
A16: ( len (Line (G,j)) = m + 1 & dom (Line (G,j)) = Seg (len (Line (G,j))) ) by A2, FINSEQ_1:def_3, MATRIX_1:def_7;
assume ( 1 <= j & j <= len (Col ((DelCol (G,i)),k)) ) ; ::_thesis: (Col ((DelCol (G,i)),k)) . j = (Col (G,(k + 1))) . j
then A17: j in dom (DelCol (G,i)) by A6, FINSEQ_3:25;
hence (Col ((DelCol (G,i)),k)) . j = (DelCol (G,i)) * (j,k) by MATRIX_1:def_8
.= (Del ((Line (G,j)),i)) . k by A1, A14, A7, A8, A17, A15, Th12
.= (Line (G,j)) . (k + 1) by A1, A2, A4, A5, A16, FINSEQ_3:111
.= (Col (G,(k + 1))) . j by A10, A8, A17, A15, Th2 ;
::_thesis: verum
end;
hence ( Col ((DelCol (G,i)),k) = Col (G,(k + 1)) & k in Seg (width (DelCol (G,i))) & k + 1 in Seg (width G) ) by A2, A5, A13, A9, A11, A6, A12, A8, FINSEQ_1:1, FINSEQ_1:14; ::_thesis: verum
end;
theorem Th15: :: GOBOARD1:15
for i, m, n, k being Element of NAT
for G being Go-board st i in Seg (width G) & width G = m + 1 & m > 0 & n in dom G & 1 <= k & k < i holds
( (DelCol (G,i)) * (n,k) = G * (n,k) & k in Seg (width G) )
proof
let i, m, n, k be Element of NAT ; ::_thesis: for G being Go-board st i in Seg (width G) & width G = m + 1 & m > 0 & n in dom G & 1 <= k & k < i holds
( (DelCol (G,i)) * (n,k) = G * (n,k) & k in Seg (width G) )
let G be Go-board; ::_thesis: ( i in Seg (width G) & width G = m + 1 & m > 0 & n in dom G & 1 <= k & k < i implies ( (DelCol (G,i)) * (n,k) = G * (n,k) & k in Seg (width G) ) )
assume that
A1: i in Seg (width G) and
A2: ( width G = m + 1 & m > 0 ) and
A3: n in dom G and
A4: ( 1 <= k & k < i ) ; ::_thesis: ( (DelCol (G,i)) * (n,k) = G * (n,k) & k in Seg (width G) )
1 < width G by A2, SEQM_3:43;
then A5: len (DelCol (G,i)) = len G by A1, Def8;
A6: ( dom G = Seg (len G) & Seg (len (DelCol (G,i))) = dom (DelCol (G,i)) ) by FINSEQ_1:def_3;
Col ((DelCol (G,i)),k) = Col (G,k) by A1, A2, A4, Th13;
hence (DelCol (G,i)) * (n,k) = (Col (G,k)) . n by A3, A6, A5, MATRIX_1:def_8
.= G * (n,k) by A3, MATRIX_1:def_8 ;
::_thesis: k in Seg (width G)
thus k in Seg (width G) by A1, A2, A4, Th13; ::_thesis: verum
end;
theorem Th16: :: GOBOARD1:16
for i, m, n, k being Element of NAT
for G being Go-board st i in Seg (width G) & width G = m + 1 & m > 0 & n in dom G & i <= k & k <= m holds
( (DelCol (G,i)) * (n,k) = G * (n,(k + 1)) & k + 1 in Seg (width G) )
proof
let i, m, n, k be Element of NAT ; ::_thesis: for G being Go-board st i in Seg (width G) & width G = m + 1 & m > 0 & n in dom G & i <= k & k <= m holds
( (DelCol (G,i)) * (n,k) = G * (n,(k + 1)) & k + 1 in Seg (width G) )
let G be Go-board; ::_thesis: ( i in Seg (width G) & width G = m + 1 & m > 0 & n in dom G & i <= k & k <= m implies ( (DelCol (G,i)) * (n,k) = G * (n,(k + 1)) & k + 1 in Seg (width G) ) )
assume that
A1: i in Seg (width G) and
A2: ( width G = m + 1 & m > 0 ) and
A3: n in dom G and
A4: ( i <= k & k <= m ) ; ::_thesis: ( (DelCol (G,i)) * (n,k) = G * (n,(k + 1)) & k + 1 in Seg (width G) )
1 < width G by A2, SEQM_3:43;
then A5: len (DelCol (G,i)) = len G by A1, Def8;
A6: ( dom G = Seg (len G) & Seg (len (DelCol (G,i))) = dom (DelCol (G,i)) ) by FINSEQ_1:def_3;
Col ((DelCol (G,i)),k) = Col (G,(k + 1)) by A1, A2, A4, Th14;
hence (DelCol (G,i)) * (n,k) = (Col (G,(k + 1))) . n by A3, A6, A5, MATRIX_1:def_8
.= G * (n,(k + 1)) by A3, MATRIX_1:def_8 ;
::_thesis: k + 1 in Seg (width G)
thus k + 1 in Seg (width G) by A1, A2, A4, Th14; ::_thesis: verum
end;
theorem :: GOBOARD1:17
for m, k being Element of NAT
for G being Go-board st width G = m + 1 & m > 0 & k in Seg m holds
( Col ((DelCol (G,1)),k) = Col (G,(k + 1)) & k in Seg (width (DelCol (G,1))) & k + 1 in Seg (width G) )
proof
let m, k be Element of NAT ; ::_thesis: for G being Go-board st width G = m + 1 & m > 0 & k in Seg m holds
( Col ((DelCol (G,1)),k) = Col (G,(k + 1)) & k in Seg (width (DelCol (G,1))) & k + 1 in Seg (width G) )
let G be Go-board; ::_thesis: ( width G = m + 1 & m > 0 & k in Seg m implies ( Col ((DelCol (G,1)),k) = Col (G,(k + 1)) & k in Seg (width (DelCol (G,1))) & k + 1 in Seg (width G) ) )
assume that
A1: width G = m + 1 and
A2: m > 0 and
A3: k in Seg m ; ::_thesis: ( Col ((DelCol (G,1)),k) = Col (G,(k + 1)) & k in Seg (width (DelCol (G,1))) & k + 1 in Seg (width G) )
1 <= width G by A1, A2, SEQM_3:43;
then A4: 1 in Seg (width G) by FINSEQ_1:1;
( 1 <= k & k <= m ) by A3, FINSEQ_1:1;
hence ( Col ((DelCol (G,1)),k) = Col (G,(k + 1)) & k in Seg (width (DelCol (G,1))) & k + 1 in Seg (width G) ) by A1, A4, Th14; ::_thesis: verum
end;
theorem :: GOBOARD1:18
for m, k, n being Element of NAT
for G being Go-board st width G = m + 1 & m > 0 & k in Seg m & n in dom G holds
( (DelCol (G,1)) * (n,k) = G * (n,(k + 1)) & 1 in Seg (width G) )
proof
let m, k, n be Element of NAT ; ::_thesis: for G being Go-board st width G = m + 1 & m > 0 & k in Seg m & n in dom G holds
( (DelCol (G,1)) * (n,k) = G * (n,(k + 1)) & 1 in Seg (width G) )
let G be Go-board; ::_thesis: ( width G = m + 1 & m > 0 & k in Seg m & n in dom G implies ( (DelCol (G,1)) * (n,k) = G * (n,(k + 1)) & 1 in Seg (width G) ) )
assume that
A1: width G = m + 1 and
A2: m > 0 and
A3: k in Seg m and
A4: n in dom G ; ::_thesis: ( (DelCol (G,1)) * (n,k) = G * (n,(k + 1)) & 1 in Seg (width G) )
1 <= width G by A1, A2, SEQM_3:43;
then A5: 1 in Seg (width G) by FINSEQ_1:1;
( 1 <= k & k <= m ) by A3, FINSEQ_1:1;
hence ( (DelCol (G,1)) * (n,k) = G * (n,(k + 1)) & 1 in Seg (width G) ) by A1, A4, A5, Th16; ::_thesis: verum
end;
theorem :: GOBOARD1:19
for m, k being Element of NAT
for G being Go-board st width G = m + 1 & m > 0 & k in Seg m holds
( Col ((DelCol (G,(width G))),k) = Col (G,k) & k in Seg (width (DelCol (G,(width G)))) )
proof
let m, k be Element of NAT ; ::_thesis: for G being Go-board st width G = m + 1 & m > 0 & k in Seg m holds
( Col ((DelCol (G,(width G))),k) = Col (G,k) & k in Seg (width (DelCol (G,(width G)))) )
let G be Go-board; ::_thesis: ( width G = m + 1 & m > 0 & k in Seg m implies ( Col ((DelCol (G,(width G))),k) = Col (G,k) & k in Seg (width (DelCol (G,(width G)))) ) )
assume that
A1: width G = m + 1 and
A2: m > 0 and
A3: k in Seg m ; ::_thesis: ( Col ((DelCol (G,(width G))),k) = Col (G,k) & k in Seg (width (DelCol (G,(width G)))) )
k <= m by A3, FINSEQ_1:1;
then A4: k < width G by A1, NAT_1:13;
1 <= width G by A1, A2, SEQM_3:43;
then A5: width G in Seg (width G) by FINSEQ_1:1;
1 <= k by A3, FINSEQ_1:1;
hence ( Col ((DelCol (G,(width G))),k) = Col (G,k) & k in Seg (width (DelCol (G,(width G)))) ) by A1, A2, A5, A4, Th13; ::_thesis: verum
end;
theorem Th20: :: GOBOARD1:20
for m, k, n being Element of NAT
for G being Go-board st width G = m + 1 & m > 0 & k in Seg m & n in dom G holds
( k in Seg (width G) & (DelCol (G,(width G))) * (n,k) = G * (n,k) & width G in Seg (width G) )
proof
let m, k, n be Element of NAT ; ::_thesis: for G being Go-board st width G = m + 1 & m > 0 & k in Seg m & n in dom G holds
( k in Seg (width G) & (DelCol (G,(width G))) * (n,k) = G * (n,k) & width G in Seg (width G) )
let G be Go-board; ::_thesis: ( width G = m + 1 & m > 0 & k in Seg m & n in dom G implies ( k in Seg (width G) & (DelCol (G,(width G))) * (n,k) = G * (n,k) & width G in Seg (width G) ) )
assume that
A1: width G = m + 1 and
A2: m > 0 and
A3: k in Seg m and
A4: n in dom G ; ::_thesis: ( k in Seg (width G) & (DelCol (G,(width G))) * (n,k) = G * (n,k) & width G in Seg (width G) )
k <= m by A3, FINSEQ_1:1;
then A5: k < width G by A1, NAT_1:13;
1 <= width G by A1, A2, SEQM_3:43;
then A6: width G in Seg (width G) by FINSEQ_1:1;
1 <= k by A3, FINSEQ_1:1;
hence ( k in Seg (width G) & (DelCol (G,(width G))) * (n,k) = G * (n,k) & width G in Seg (width G) ) by A1, A2, A4, A6, A5, Th15; ::_thesis: verum
end;
theorem :: GOBOARD1:21
for f being FinSequence of (TOP-REAL 2)
for i, n, m being Element of NAT
for G being Go-board st rng f misses rng (Col (G,i)) & f /. n in rng (Line (G,m)) & n in dom f & i in Seg (width G) & m in dom G & width G > 1 holds
f /. n in rng (Line ((DelCol (G,i)),m))
proof
let f be FinSequence of (TOP-REAL 2); ::_thesis: for i, n, m being Element of NAT
for G being Go-board st rng f misses rng (Col (G,i)) & f /. n in rng (Line (G,m)) & n in dom f & i in Seg (width G) & m in dom G & width G > 1 holds
f /. n in rng (Line ((DelCol (G,i)),m))
let i, n, m be Element of NAT ; ::_thesis: for G being Go-board st rng f misses rng (Col (G,i)) & f /. n in rng (Line (G,m)) & n in dom f & i in Seg (width G) & m in dom G & width G > 1 holds
f /. n in rng (Line ((DelCol (G,i)),m))
let G be Go-board; ::_thesis: ( rng f misses rng (Col (G,i)) & f /. n in rng (Line (G,m)) & n in dom f & i in Seg (width G) & m in dom G & width G > 1 implies f /. n in rng (Line ((DelCol (G,i)),m)) )
set D = DelCol (G,i);
assume that
A1: rng f misses rng (Col (G,i)) and
A2: f /. n in rng (Line (G,m)) and
A3: n in dom f and
A4: i in Seg (width G) and
A5: m in dom G and
A6: width G > 1 ; ::_thesis: f /. n in rng (Line ((DelCol (G,i)),m))
A7: ( len (Line ((DelCol (G,i)),m)) = width (DelCol (G,i)) & dom (Line ((DelCol (G,i)),m)) = Seg (len (Line ((DelCol (G,i)),m))) ) by FINSEQ_1:def_3, MATRIX_1:def_7;
consider j being Nat such that
A8: j in dom (Line (G,m)) and
A9: f /. n = (Line (G,m)) . j by A2, FINSEQ_2:10;
reconsider j = j as Element of NAT by ORDINAL1:def_12;
A10: len (Line (G,m)) = width G by MATRIX_1:def_7;
then A11: j <= width G by A8, FINSEQ_3:25;
A12: dom (Line (G,m)) = Seg (len (Line (G,m))) by FINSEQ_1:def_3;
then A13: 1 <= i by A4, A10, FINSEQ_3:25;
A14: f /. n = G * (m,j) by A8, A9, A12, A10, MATRIX_1:def_7;
A15: i <= width G by A4, A12, A10, FINSEQ_3:25;
A16: 1 <= j by A8, FINSEQ_3:25;
consider M being Element of NAT such that
A17: width G = M + 1 and
A18: M > 0 by A6, SEQM_3:43;
A19: width (DelCol (G,i)) = M by A4, A17, A18, Th10;
percases ( j < i or i < j ) by A1, A3, A5, A14, Th8, XXREAL_0:1;
supposeA20: j < i ; ::_thesis: f /. n in rng (Line ((DelCol (G,i)),m))
then j < width G by A15, XXREAL_0:2;
then j <= M by A17, NAT_1:13;
then A21: j in Seg (width (DelCol (G,i))) by A16, A19, FINSEQ_1:1;
f /. n = (DelCol (G,i)) * (m,j) by A4, A5, A14, A16, A17, A18, A20, Th15;
then (Line ((DelCol (G,i)),m)) . j = f /. n by A21, MATRIX_1:def_7;
hence f /. n in rng (Line ((DelCol (G,i)),m)) by A7, A21, FUNCT_1:def_3; ::_thesis: verum
end;
supposeA22: i < j ; ::_thesis: f /. n in rng (Line ((DelCol (G,i)),m))
reconsider l = j - 1 as Element of NAT by A16, INT_1:5;
A23: l <= M by A11, A17, XREAL_1:20;
i + 1 <= j by A22, NAT_1:13;
then A24: i <= l by XREAL_1:19;
then 1 <= l by A13, XXREAL_0:2;
then A25: l in Seg (width (DelCol (G,i))) by A19, A23, FINSEQ_1:1;
l + 1 = j ;
then f /. n = (DelCol (G,i)) * (m,l) by A4, A5, A14, A13, A17, A24, A23, Th16;
then (Line ((DelCol (G,i)),m)) . l = f /. n by A25, MATRIX_1:def_7;
hence f /. n in rng (Line ((DelCol (G,i)),m)) by A7, A25, FUNCT_1:def_3; ::_thesis: verum
end;
end;
end;
definition
let D be set ;
let f be FinSequence of D;
let M be Matrix of D;
predf is_sequence_on M means :Def9: :: GOBOARD1:def 9
( ( for n being Element of NAT st n in dom f holds
ex i, j being Element of NAT st
( [i,j] in Indices M & f /. n = M * (i,j) ) ) & ( for n being Element of NAT st n in dom f & n + 1 in dom f holds
for m, k, i, j being Element of NAT st [m,k] in Indices M & [i,j] in Indices M & f /. n = M * (m,k) & f /. (n + 1) = M * (i,j) holds
(abs (m - i)) + (abs (k - j)) = 1 ) );
end;
:: deftheorem Def9 defines is_sequence_on GOBOARD1:def_9_:_
for D being set
for f being FinSequence of D
for M being Matrix of D holds
( f is_sequence_on M iff ( ( for n being Element of NAT st n in dom f holds
ex i, j being Element of NAT st
( [i,j] in Indices M & f /. n = M * (i,j) ) ) & ( for n being Element of NAT st n in dom f & n + 1 in dom f holds
for m, k, i, j being Element of NAT st [m,k] in Indices M & [i,j] in Indices M & f /. n = M * (m,k) & f /. (n + 1) = M * (i,j) holds
(abs (m - i)) + (abs (k - j)) = 1 ) ) );
Lm2: for D being set
for M being Matrix of D holds <*> D is_sequence_on M
proof
let D be set ; ::_thesis: for M being Matrix of D holds <*> D is_sequence_on M
let M be Matrix of D; ::_thesis: <*> D is_sequence_on M
set f = <*> D;
thus ( ( for n being Element of NAT st n in dom (<*> D) holds
ex i, j being Element of NAT st
( [i,j] in Indices M & (<*> D) /. n = M * (i,j) ) ) & ( for n being Element of NAT st n in dom (<*> D) & n + 1 in dom (<*> D) holds
for m, k, i, j being Element of NAT st [m,k] in Indices M & [i,j] in Indices M & (<*> D) /. n = M * (m,k) & (<*> D) /. (n + 1) = M * (i,j) holds
(abs (m - i)) + (abs (k - j)) = 1 ) ) ; :: according to GOBOARD1:def_9 ::_thesis: verum
end;
theorem :: GOBOARD1:22
for m being Element of NAT
for D being set
for f being FinSequence of D
for M being Matrix of D holds
( ( m in dom f implies 1 <= len (f | m) ) & ( f is_sequence_on M implies f | m is_sequence_on M ) )
proof
let m be Element of NAT ; ::_thesis: for D being set
for f being FinSequence of D
for M being Matrix of D holds
( ( m in dom f implies 1 <= len (f | m) ) & ( f is_sequence_on M implies f | m is_sequence_on M ) )
let D be set ; ::_thesis: for f being FinSequence of D
for M being Matrix of D holds
( ( m in dom f implies 1 <= len (f | m) ) & ( f is_sequence_on M implies f | m is_sequence_on M ) )
let f be FinSequence of D; ::_thesis: for M being Matrix of D holds
( ( m in dom f implies 1 <= len (f | m) ) & ( f is_sequence_on M implies f | m is_sequence_on M ) )
let M be Matrix of D; ::_thesis: ( ( m in dom f implies 1 <= len (f | m) ) & ( f is_sequence_on M implies f | m is_sequence_on M ) )
set g = f | m;
thus ( m in dom f implies 1 <= len (f | m) ) ::_thesis: ( f is_sequence_on M implies f | m is_sequence_on M )
proof
assume m in dom f ; ::_thesis: 1 <= len (f | m)
then ( 1 <= m & m <= len f ) by FINSEQ_3:25;
hence 1 <= len (f | m) by FINSEQ_1:59; ::_thesis: verum
end;
assume A1: f is_sequence_on M ; ::_thesis: f | m is_sequence_on M
percases ( m < 1 or m >= len f or ( 1 <= m & m < len f ) ) ;
supposeA2: m < 1 ; ::_thesis: f | m is_sequence_on M
A3: f | 0 = <*> D ;
m = 0 by A2, NAT_1:14;
hence f | m is_sequence_on M by A3, Lm2; ::_thesis: verum
end;
suppose m >= len f ; ::_thesis: f | m is_sequence_on M
hence f | m is_sequence_on M by A1, FINSEQ_1:58; ::_thesis: verum
end;
supposeA4: ( 1 <= m & m < len f ) ; ::_thesis: f | m is_sequence_on M
A5: dom (f | m) = Seg (len (f | m)) by FINSEQ_1:def_3;
A6: ( m in dom f & len (f | m) = m ) by A4, FINSEQ_1:59, FINSEQ_3:25;
A7: now__::_thesis:_for_n_being_Element_of_NAT_st_n_in_dom_(f_|_m)_&_n_+_1_in_dom_(f_|_m)_holds_
for_i1,_i2,_j1,_j2_being_Element_of_NAT_st_[i1,i2]_in_Indices_M_&_[j1,j2]_in_Indices_M_&_(f_|_m)_/._n_=_M_*_(i1,i2)_&_(f_|_m)_/._(n_+_1)_=_M_*_(j1,j2)_holds_
(abs_(i1_-_j1))_+_(abs_(i2_-_j2))_=_1
let n be Element of NAT ; ::_thesis: ( n in dom (f | m) & n + 1 in dom (f | m) implies for i1, i2, j1, j2 being Element of NAT st [i1,i2] in Indices M & [j1,j2] in Indices M & (f | m) /. n = M * (i1,i2) & (f | m) /. (n + 1) = M * (j1,j2) holds
(abs (i1 - j1)) + (abs (i2 - j2)) = 1 )
assume A8: ( n in dom (f | m) & n + 1 in dom (f | m) ) ; ::_thesis: for i1, i2, j1, j2 being Element of NAT st [i1,i2] in Indices M & [j1,j2] in Indices M & (f | m) /. n = M * (i1,i2) & (f | m) /. (n + 1) = M * (j1,j2) holds
(abs (i1 - j1)) + (abs (i2 - j2)) = 1
then A9: ( n in dom f & n + 1 in dom f ) by A5, A6, FINSEQ_4:71;
let i1, i2, j1, j2 be Element of NAT ; ::_thesis: ( [i1,i2] in Indices M & [j1,j2] in Indices M & (f | m) /. n = M * (i1,i2) & (f | m) /. (n + 1) = M * (j1,j2) implies (abs (i1 - j1)) + (abs (i2 - j2)) = 1 )
assume A10: ( [i1,i2] in Indices M & [j1,j2] in Indices M & (f | m) /. n = M * (i1,i2) & (f | m) /. (n + 1) = M * (j1,j2) ) ; ::_thesis: (abs (i1 - j1)) + (abs (i2 - j2)) = 1
( (f | m) /. n = f /. n & (f | m) /. (n + 1) = f /. (n + 1) ) by A5, A6, A8, FINSEQ_4:71;
hence (abs (i1 - j1)) + (abs (i2 - j2)) = 1 by A1, A9, A10, Def9; ::_thesis: verum
end;
now__::_thesis:_for_n_being_Element_of_NAT_st_n_in_dom_(f_|_m)_holds_
ex_i,_j_being_Element_of_NAT_st_
(_[i,j]_in_Indices_M_&_(f_|_m)_/._n_=_M_*_(i,j)_)
let n be Element of NAT ; ::_thesis: ( n in dom (f | m) implies ex i, j being Element of NAT st
( [i,j] in Indices M & (f | m) /. n = M * (i,j) ) )
assume A11: n in dom (f | m) ; ::_thesis: ex i, j being Element of NAT st
( [i,j] in Indices M & (f | m) /. n = M * (i,j) )
then n in dom f by A5, A6, FINSEQ_4:71;
then consider i, j being Element of NAT such that
A12: ( [i,j] in Indices M & f /. n = M * (i,j) ) by A1, Def9;
take i = i; ::_thesis: ex j being Element of NAT st
( [i,j] in Indices M & (f | m) /. n = M * (i,j) )
take j = j; ::_thesis: ( [i,j] in Indices M & (f | m) /. n = M * (i,j) )
thus ( [i,j] in Indices M & (f | m) /. n = M * (i,j) ) by A5, A6, A11, A12, FINSEQ_4:71; ::_thesis: verum
end;
hence f | m is_sequence_on M by A7, Def9; ::_thesis: verum
end;
end;
end;
theorem :: GOBOARD1:23
for f1, f2 being FinSequence of (TOP-REAL 2)
for D being set
for M being Matrix of D st ( for n being Element of NAT st n in dom f1 holds
ex i, j being Element of NAT st
( [i,j] in Indices M & f1 /. n = M * (i,j) ) ) & ( for n being Element of NAT st n in dom f2 holds
ex i, j being Element of NAT st
( [i,j] in Indices M & f2 /. n = M * (i,j) ) ) holds
for n being Element of NAT st n in dom (f1 ^ f2) holds
ex i, j being Element of NAT st
( [i,j] in Indices M & (f1 ^ f2) /. n = M * (i,j) )
proof
let f1, f2 be FinSequence of (TOP-REAL 2); ::_thesis: for D being set
for M being Matrix of D st ( for n being Element of NAT st n in dom f1 holds
ex i, j being Element of NAT st
( [i,j] in Indices M & f1 /. n = M * (i,j) ) ) & ( for n being Element of NAT st n in dom f2 holds
ex i, j being Element of NAT st
( [i,j] in Indices M & f2 /. n = M * (i,j) ) ) holds
for n being Element of NAT st n in dom (f1 ^ f2) holds
ex i, j being Element of NAT st
( [i,j] in Indices M & (f1 ^ f2) /. n = M * (i,j) )
let D be set ; ::_thesis: for M being Matrix of D st ( for n being Element of NAT st n in dom f1 holds
ex i, j being Element of NAT st
( [i,j] in Indices M & f1 /. n = M * (i,j) ) ) & ( for n being Element of NAT st n in dom f2 holds
ex i, j being Element of NAT st
( [i,j] in Indices M & f2 /. n = M * (i,j) ) ) holds
for n being Element of NAT st n in dom (f1 ^ f2) holds
ex i, j being Element of NAT st
( [i,j] in Indices M & (f1 ^ f2) /. n = M * (i,j) )
let M be Matrix of D; ::_thesis: ( ( for n being Element of NAT st n in dom f1 holds
ex i, j being Element of NAT st
( [i,j] in Indices M & f1 /. n = M * (i,j) ) ) & ( for n being Element of NAT st n in dom f2 holds
ex i, j being Element of NAT st
( [i,j] in Indices M & f2 /. n = M * (i,j) ) ) implies for n being Element of NAT st n in dom (f1 ^ f2) holds
ex i, j being Element of NAT st
( [i,j] in Indices M & (f1 ^ f2) /. n = M * (i,j) ) )
assume that
A1: for n being Element of NAT st n in dom f1 holds
ex i, j being Element of NAT st
( [i,j] in Indices M & f1 /. n = M * (i,j) ) and
A2: for n being Element of NAT st n in dom f2 holds
ex i, j being Element of NAT st
( [i,j] in Indices M & f2 /. n = M * (i,j) ) ; ::_thesis: for n being Element of NAT st n in dom (f1 ^ f2) holds
ex i, j being Element of NAT st
( [i,j] in Indices M & (f1 ^ f2) /. n = M * (i,j) )
let n be Element of NAT ; ::_thesis: ( n in dom (f1 ^ f2) implies ex i, j being Element of NAT st
( [i,j] in Indices M & (f1 ^ f2) /. n = M * (i,j) ) )
assume A3: n in dom (f1 ^ f2) ; ::_thesis: ex i, j being Element of NAT st
( [i,j] in Indices M & (f1 ^ f2) /. n = M * (i,j) )
percases ( n in dom f1 or ex m being Nat st
( m in dom f2 & n = (len f1) + m ) ) by A3, FINSEQ_1:25;
supposeA4: n in dom f1 ; ::_thesis: ex i, j being Element of NAT st
( [i,j] in Indices M & (f1 ^ f2) /. n = M * (i,j) )
then consider i, j being Element of NAT such that
A5: [i,j] in Indices M and
A6: f1 /. n = M * (i,j) by A1;
take i ; ::_thesis: ex j being Element of NAT st
( [i,j] in Indices M & (f1 ^ f2) /. n = M * (i,j) )
take j ; ::_thesis: ( [i,j] in Indices M & (f1 ^ f2) /. n = M * (i,j) )
thus [i,j] in Indices M by A5; ::_thesis: (f1 ^ f2) /. n = M * (i,j)
thus (f1 ^ f2) /. n = M * (i,j) by A4, A6, FINSEQ_4:68; ::_thesis: verum
end;
suppose ex m being Nat st
( m in dom f2 & n = (len f1) + m ) ; ::_thesis: ex i, j being Element of NAT st
( [i,j] in Indices M & (f1 ^ f2) /. n = M * (i,j) )
then consider m being Nat such that
A7: m in dom f2 and
A8: n = (len f1) + m ;
consider i, j being Element of NAT such that
A9: [i,j] in Indices M and
A10: f2 /. m = M * (i,j) by A2, A7;
take i ; ::_thesis: ex j being Element of NAT st
( [i,j] in Indices M & (f1 ^ f2) /. n = M * (i,j) )
take j ; ::_thesis: ( [i,j] in Indices M & (f1 ^ f2) /. n = M * (i,j) )
thus [i,j] in Indices M by A9; ::_thesis: (f1 ^ f2) /. n = M * (i,j)
thus (f1 ^ f2) /. n = M * (i,j) by A7, A8, A10, FINSEQ_4:69; ::_thesis: verum
end;
end;
end;
theorem :: GOBOARD1:24
for f1, f2 being FinSequence of (TOP-REAL 2)
for D being set
for M being Matrix of D st ( for n being Element of NAT st n in dom f1 & n + 1 in dom f1 holds
for m, k, i, j being Element of NAT st [m,k] in Indices M & [i,j] in Indices M & f1 /. n = M * (m,k) & f1 /. (n + 1) = M * (i,j) holds
(abs (m - i)) + (abs (k - j)) = 1 ) & ( for n being Element of NAT st n in dom f2 & n + 1 in dom f2 holds
for m, k, i, j being Element of NAT st [m,k] in Indices M & [i,j] in Indices M & f2 /. n = M * (m,k) & f2 /. (n + 1) = M * (i,j) holds
(abs (m - i)) + (abs (k - j)) = 1 ) & ( for m, k, i, j being Element of NAT st [m,k] in Indices M & [i,j] in Indices M & f1 /. (len f1) = M * (m,k) & f2 /. 1 = M * (i,j) & len f1 in dom f1 & 1 in dom f2 holds
(abs (m - i)) + (abs (k - j)) = 1 ) holds
for n being Element of NAT st n in dom (f1 ^ f2) & n + 1 in dom (f1 ^ f2) holds
for m, k, i, j being Element of NAT st [m,k] in Indices M & [i,j] in Indices M & (f1 ^ f2) /. n = M * (m,k) & (f1 ^ f2) /. (n + 1) = M * (i,j) holds
(abs (m - i)) + (abs (k - j)) = 1
proof
let f1, f2 be FinSequence of (TOP-REAL 2); ::_thesis: for D being set
for M being Matrix of D st ( for n being Element of NAT st n in dom f1 & n + 1 in dom f1 holds
for m, k, i, j being Element of NAT st [m,k] in Indices M & [i,j] in Indices M & f1 /. n = M * (m,k) & f1 /. (n + 1) = M * (i,j) holds
(abs (m - i)) + (abs (k - j)) = 1 ) & ( for n being Element of NAT st n in dom f2 & n + 1 in dom f2 holds
for m, k, i, j being Element of NAT st [m,k] in Indices M & [i,j] in Indices M & f2 /. n = M * (m,k) & f2 /. (n + 1) = M * (i,j) holds
(abs (m - i)) + (abs (k - j)) = 1 ) & ( for m, k, i, j being Element of NAT st [m,k] in Indices M & [i,j] in Indices M & f1 /. (len f1) = M * (m,k) & f2 /. 1 = M * (i,j) & len f1 in dom f1 & 1 in dom f2 holds
(abs (m - i)) + (abs (k - j)) = 1 ) holds
for n being Element of NAT st n in dom (f1 ^ f2) & n + 1 in dom (f1 ^ f2) holds
for m, k, i, j being Element of NAT st [m,k] in Indices M & [i,j] in Indices M & (f1 ^ f2) /. n = M * (m,k) & (f1 ^ f2) /. (n + 1) = M * (i,j) holds
(abs (m - i)) + (abs (k - j)) = 1
let D be set ; ::_thesis: for M being Matrix of D st ( for n being Element of NAT st n in dom f1 & n + 1 in dom f1 holds
for m, k, i, j being Element of NAT st [m,k] in Indices M & [i,j] in Indices M & f1 /. n = M * (m,k) & f1 /. (n + 1) = M * (i,j) holds
(abs (m - i)) + (abs (k - j)) = 1 ) & ( for n being Element of NAT st n in dom f2 & n + 1 in dom f2 holds
for m, k, i, j being Element of NAT st [m,k] in Indices M & [i,j] in Indices M & f2 /. n = M * (m,k) & f2 /. (n + 1) = M * (i,j) holds
(abs (m - i)) + (abs (k - j)) = 1 ) & ( for m, k, i, j being Element of NAT st [m,k] in Indices M & [i,j] in Indices M & f1 /. (len f1) = M * (m,k) & f2 /. 1 = M * (i,j) & len f1 in dom f1 & 1 in dom f2 holds
(abs (m - i)) + (abs (k - j)) = 1 ) holds
for n being Element of NAT st n in dom (f1 ^ f2) & n + 1 in dom (f1 ^ f2) holds
for m, k, i, j being Element of NAT st [m,k] in Indices M & [i,j] in Indices M & (f1 ^ f2) /. n = M * (m,k) & (f1 ^ f2) /. (n + 1) = M * (i,j) holds
(abs (m - i)) + (abs (k - j)) = 1
let M be Matrix of D; ::_thesis: ( ( for n being Element of NAT st n in dom f1 & n + 1 in dom f1 holds
for m, k, i, j being Element of NAT st [m,k] in Indices M & [i,j] in Indices M & f1 /. n = M * (m,k) & f1 /. (n + 1) = M * (i,j) holds
(abs (m - i)) + (abs (k - j)) = 1 ) & ( for n being Element of NAT st n in dom f2 & n + 1 in dom f2 holds
for m, k, i, j being Element of NAT st [m,k] in Indices M & [i,j] in Indices M & f2 /. n = M * (m,k) & f2 /. (n + 1) = M * (i,j) holds
(abs (m - i)) + (abs (k - j)) = 1 ) & ( for m, k, i, j being Element of NAT st [m,k] in Indices M & [i,j] in Indices M & f1 /. (len f1) = M * (m,k) & f2 /. 1 = M * (i,j) & len f1 in dom f1 & 1 in dom f2 holds
(abs (m - i)) + (abs (k - j)) = 1 ) implies for n being Element of NAT st n in dom (f1 ^ f2) & n + 1 in dom (f1 ^ f2) holds
for m, k, i, j being Element of NAT st [m,k] in Indices M & [i,j] in Indices M & (f1 ^ f2) /. n = M * (m,k) & (f1 ^ f2) /. (n + 1) = M * (i,j) holds
(abs (m - i)) + (abs (k - j)) = 1 )
assume that
A1: for n being Element of NAT st n in dom f1 & n + 1 in dom f1 holds
for m, k, i, j being Element of NAT st [m,k] in Indices M & [i,j] in Indices M & f1 /. n = M * (m,k) & f1 /. (n + 1) = M * (i,j) holds
(abs (m - i)) + (abs (k - j)) = 1 and
A2: for n being Element of NAT st n in dom f2 & n + 1 in dom f2 holds
for m, k, i, j being Element of NAT st [m,k] in Indices M & [i,j] in Indices M & f2 /. n = M * (m,k) & f2 /. (n + 1) = M * (i,j) holds
(abs (m - i)) + (abs (k - j)) = 1 and
A3: for m, k, i, j being Element of NAT st [m,k] in Indices M & [i,j] in Indices M & f1 /. (len f1) = M * (m,k) & f2 /. 1 = M * (i,j) & len f1 in dom f1 & 1 in dom f2 holds
(abs (m - i)) + (abs (k - j)) = 1 ; ::_thesis: for n being Element of NAT st n in dom (f1 ^ f2) & n + 1 in dom (f1 ^ f2) holds
for m, k, i, j being Element of NAT st [m,k] in Indices M & [i,j] in Indices M & (f1 ^ f2) /. n = M * (m,k) & (f1 ^ f2) /. (n + 1) = M * (i,j) holds
(abs (m - i)) + (abs (k - j)) = 1
let n be Element of NAT ; ::_thesis: ( n in dom (f1 ^ f2) & n + 1 in dom (f1 ^ f2) implies for m, k, i, j being Element of NAT st [m,k] in Indices M & [i,j] in Indices M & (f1 ^ f2) /. n = M * (m,k) & (f1 ^ f2) /. (n + 1) = M * (i,j) holds
(abs (m - i)) + (abs (k - j)) = 1 )
assume that
A4: n in dom (f1 ^ f2) and
A5: n + 1 in dom (f1 ^ f2) ; ::_thesis: for m, k, i, j being Element of NAT st [m,k] in Indices M & [i,j] in Indices M & (f1 ^ f2) /. n = M * (m,k) & (f1 ^ f2) /. (n + 1) = M * (i,j) holds
(abs (m - i)) + (abs (k - j)) = 1
let m, k, i, j be Element of NAT ; ::_thesis: ( [m,k] in Indices M & [i,j] in Indices M & (f1 ^ f2) /. n = M * (m,k) & (f1 ^ f2) /. (n + 1) = M * (i,j) implies (abs (m - i)) + (abs (k - j)) = 1 )
assume that
A6: ( [m,k] in Indices M & [i,j] in Indices M ) and
A7: (f1 ^ f2) /. n = M * (m,k) and
A8: (f1 ^ f2) /. (n + 1) = M * (i,j) ; ::_thesis: (abs (m - i)) + (abs (k - j)) = 1
A9: dom f1 = Seg (len f1) by FINSEQ_1:def_3;
percases ( n in dom f1 or ex m being Nat st
( m in dom f2 & n = (len f1) + m ) ) by A4, FINSEQ_1:25;
supposeA10: n in dom f1 ; ::_thesis: (abs (m - i)) + (abs (k - j)) = 1
then A11: f1 /. n = M * (m,k) by A7, FINSEQ_4:68;
now__::_thesis:_(abs_(m_-_i))_+_(abs_(k_-_j))_=_1
percases ( n + 1 in dom f1 or ex m being Nat st
( m in dom f2 & n + 1 = (len f1) + m ) ) by A5, FINSEQ_1:25;
supposeA12: n + 1 in dom f1 ; ::_thesis: (abs (m - i)) + (abs (k - j)) = 1
then f1 /. (n + 1) = M * (i,j) by A8, FINSEQ_4:68;
hence (abs (m - i)) + (abs (k - j)) = 1 by A1, A6, A10, A11, A12; ::_thesis: verum
end;
suppose ex m being Nat st
( m in dom f2 & n + 1 = (len f1) + m ) ; ::_thesis: (abs (m - i)) + (abs (k - j)) = 1
then consider mm being Nat such that
A13: mm in dom f2 and
A14: n + 1 = (len f1) + mm ;
1 <= mm by A13, FINSEQ_3:25;
then A15: 0 <= mm - 1 by XREAL_1:48;
(len f1) + (mm - 1) <= (len f1) + 0 by A9, A10, A14, FINSEQ_1:1;
then A16: mm - 1 = 0 by A15, XREAL_1:6;
then ( M * (i,j) = f2 /. 1 & M * (m,k) = f1 /. (len f1) ) by A7, A8, A10, A13, A14, FINSEQ_4:68, FINSEQ_4:69;
hence (abs (m - i)) + (abs (k - j)) = 1 by A3, A6, A10, A13, A14, A16; ::_thesis: verum
end;
end;
end;
hence (abs (m - i)) + (abs (k - j)) = 1 ; ::_thesis: verum
end;
suppose ex m being Nat st
( m in dom f2 & n = (len f1) + m ) ; ::_thesis: (abs (m - i)) + (abs (k - j)) = 1
then consider mm being Nat such that
A17: mm in dom f2 and
A18: n = (len f1) + mm ;
A19: M * (m,k) = f2 /. mm by A7, A17, A18, FINSEQ_4:69;
A20: ((len f1) + mm) + 1 = (len f1) + (mm + 1) ;
n + 1 <= len (f1 ^ f2) by A5, FINSEQ_3:25;
then ((len f1) + mm) + 1 <= (len f1) + (len f2) by A18, FINSEQ_1:22;
then ( 1 <= mm + 1 & mm + 1 <= len f2 ) by A20, NAT_1:11, XREAL_1:6;
then A21: mm + 1 in dom f2 by FINSEQ_3:25;
M * (i,j) = (f1 ^ f2) /. ((len f1) + (mm + 1)) by A8, A18
.= f2 /. (mm + 1) by A21, FINSEQ_4:69 ;
hence (abs (m - i)) + (abs (k - j)) = 1 by A2, A6, A17, A21, A19; ::_thesis: verum
end;
end;
end;
theorem :: GOBOARD1:25
for i being Element of NAT
for G being Go-board
for f being FinSequence of (TOP-REAL 2) st f is_sequence_on G & i in Seg (width G) & rng f misses rng (Col (G,i)) & width G > 1 holds
f is_sequence_on DelCol (G,i)
proof
let i be Element of NAT ; ::_thesis: for G being Go-board
for f being FinSequence of (TOP-REAL 2) st f is_sequence_on G & i in Seg (width G) & rng f misses rng (Col (G,i)) & width G > 1 holds
f is_sequence_on DelCol (G,i)
let G be Go-board; ::_thesis: for f being FinSequence of (TOP-REAL 2) st f is_sequence_on G & i in Seg (width G) & rng f misses rng (Col (G,i)) & width G > 1 holds
f is_sequence_on DelCol (G,i)
let f be FinSequence of (TOP-REAL 2); ::_thesis: ( f is_sequence_on G & i in Seg (width G) & rng f misses rng (Col (G,i)) & width G > 1 implies f is_sequence_on DelCol (G,i) )
set D = DelCol (G,i);
assume that
A1: f is_sequence_on G and
A2: i in Seg (width G) and
A3: rng f misses rng (Col (G,i)) and
A4: width G > 1 ; ::_thesis: f is_sequence_on DelCol (G,i)
A5: len G = len (DelCol (G,i)) by A2, A4, Def8;
A6: Indices (DelCol (G,i)) = [:(dom (DelCol (G,i))),(Seg (width (DelCol (G,i)))):] by MATRIX_1:def_4;
A7: Indices G = [:(dom G),(Seg (width G)):] by MATRIX_1:def_4;
A8: ( dom G = Seg (len G) & dom (DelCol (G,i)) = Seg (len (DelCol (G,i))) ) by FINSEQ_1:def_3;
consider M being Element of NAT such that
A9: width G = M + 1 and
A10: M > 0 by A4, SEQM_3:43;
A11: width (DelCol (G,i)) = M by A2, A9, A10, Th10;
A12: now__::_thesis:_for_n_being_Element_of_NAT_st_n_in_dom_f_&_n_+_1_in_dom_f_holds_
for_i1,_i2,_j1,_j2_being_Element_of_NAT_st_[i1,i2]_in_Indices_(DelCol_(G,i))_&_[j1,j2]_in_Indices_(DelCol_(G,i))_&_f_/._n_=_(DelCol_(G,i))_*_(i1,i2)_&_f_/._(n_+_1)_=_(DelCol_(G,i))_*_(j1,j2)_holds_
(abs_(i1_-_j1))_+_(abs_(i2_-_j2))_=_1
let n be Element of NAT ; ::_thesis: ( n in dom f & n + 1 in dom f implies for i1, i2, j1, j2 being Element of NAT st [i1,i2] in Indices (DelCol (G,i)) & [j1,j2] in Indices (DelCol (G,i)) & f /. n = (DelCol (G,i)) * (i1,i2) & f /. (n + 1) = (DelCol (G,i)) * (j1,j2) holds
(abs (i1 - j1)) + (abs (i2 - j2)) = 1 )
assume A13: ( n in dom f & n + 1 in dom f ) ; ::_thesis: for i1, i2, j1, j2 being Element of NAT st [i1,i2] in Indices (DelCol (G,i)) & [j1,j2] in Indices (DelCol (G,i)) & f /. n = (DelCol (G,i)) * (i1,i2) & f /. (n + 1) = (DelCol (G,i)) * (j1,j2) holds
(abs (i1 - j1)) + (abs (i2 - j2)) = 1
let i1, i2, j1, j2 be Element of NAT ; ::_thesis: ( [i1,i2] in Indices (DelCol (G,i)) & [j1,j2] in Indices (DelCol (G,i)) & f /. n = (DelCol (G,i)) * (i1,i2) & f /. (n + 1) = (DelCol (G,i)) * (j1,j2) implies (abs (i1 - j1)) + (abs (i2 - j2)) = 1 )
assume that
A14: [i1,i2] in Indices (DelCol (G,i)) and
A15: [j1,j2] in Indices (DelCol (G,i)) and
A16: ( f /. n = (DelCol (G,i)) * (i1,i2) & f /. (n + 1) = (DelCol (G,i)) * (j1,j2) ) ; ::_thesis: (abs (i1 - j1)) + (abs (i2 - j2)) = 1
A17: i1 in dom (DelCol (G,i)) by A6, A14, ZFMISC_1:87;
A18: i2 in Seg (width (DelCol (G,i))) by A6, A14, ZFMISC_1:87;
then A19: 1 <= i2 by FINSEQ_1:1;
A20: i2 <= M by A11, A18, FINSEQ_1:1;
then ( 1 <= i2 + 1 & i2 + 1 <= M + 1 ) by NAT_1:11, XREAL_1:6;
then i2 + 1 in Seg (M + 1) by FINSEQ_1:1;
then A21: [i1,(i2 + 1)] in Indices G by A5, A9, A8, A7, A17, ZFMISC_1:87;
A22: j1 in dom (DelCol (G,i)) by A6, A15, ZFMISC_1:87;
A23: j2 in Seg (width (DelCol (G,i))) by A6, A15, ZFMISC_1:87;
then A24: 1 <= j2 by FINSEQ_1:1;
M <= M + 1 by NAT_1:11;
then A25: Seg (width (DelCol (G,i))) c= Seg (width G) by A9, A11, FINSEQ_1:5;
then A26: [j1,j2] in Indices G by A5, A8, A7, A22, A23, ZFMISC_1:87;
A27: j2 <= M by A11, A23, FINSEQ_1:1;
then ( 1 <= j2 + 1 & j2 + 1 <= M + 1 ) by NAT_1:11, XREAL_1:6;
then j2 + 1 in Seg (M + 1) by FINSEQ_1:1;
then A28: [j1,(j2 + 1)] in Indices G by A5, A9, A8, A7, A22, ZFMISC_1:87;
A29: [i1,i2] in Indices G by A5, A8, A7, A17, A18, A25, ZFMISC_1:87;
now__::_thesis:_(_(_i2_<_i_&_j2_<_i_&_(abs_(i1_-_j1))_+_(abs_(i2_-_j2))_=_1_)_or_(_i_<=_i2_&_j2_<_i_&_contradiction_)_or_(_i2_<_i_&_i_<=_j2_&_contradiction_)_or_(_i_<=_i2_&_i_<=_j2_&_1_=_(abs_(i1_-_j1))_+_(abs_(i2_-_j2))_)_)
percases ( ( i2 < i & j2 < i ) or ( i <= i2 & j2 < i ) or ( i2 < i & i <= j2 ) or ( i <= i2 & i <= j2 ) ) ;
case ( i2 < i & j2 < i ) ; ::_thesis: (abs (i1 - j1)) + (abs (i2 - j2)) = 1
then ( f /. n = G * (i1,i2) & f /. (n + 1) = G * (j1,j2) ) by A2, A5, A9, A10, A8, A16, A17, A22, A19, A24, Th15;
hence (abs (i1 - j1)) + (abs (i2 - j2)) = 1 by A1, A13, A29, A26, Def9; ::_thesis: verum
end;
caseA30: ( i <= i2 & j2 < i ) ; ::_thesis: contradiction
i2 <= i2 + 1 by NAT_1:11;
then i <= i2 + 1 by A30, XXREAL_0:2;
then A31: j2 < i2 + 1 by A30, XXREAL_0:2;
then j2 + 1 <= i2 + 1 by NAT_1:13;
then A32: 1 <= (i2 + 1) - j2 by XREAL_1:19;
( f /. n = G * (i1,(i2 + 1)) & f /. (n + 1) = G * (j1,j2) ) by A2, A5, A9, A8, A16, A17, A22, A20, A24, A30, Th15, Th16;
then A33: 1 = (abs (i1 - j1)) + (abs ((i2 + 1) - j2)) by A1, A13, A26, A21, Def9;
0 < (i2 + 1) - j2 by A31, XREAL_1:50;
then A34: abs ((i2 + 1) - j2) = (i2 + 1) - j2 by ABSVALUE:def_1;
0 <= abs (i1 - j1) by COMPLEX1:46;
then 0 + ((i2 + 1) - j2) <= 1 by A33, A34, XREAL_1:7;
then (i2 + 1) - j2 = 1 by A32, XXREAL_0:1;
hence contradiction by A30; ::_thesis: verum
end;
caseA35: ( i2 < i & i <= j2 ) ; ::_thesis: contradiction
j2 <= j2 + 1 by NAT_1:11;
then i <= j2 + 1 by A35, XXREAL_0:2;
then A36: i2 < j2 + 1 by A35, XXREAL_0:2;
then i2 + 1 <= j2 + 1 by NAT_1:13;
then A37: 1 <= (j2 + 1) - i2 by XREAL_1:19;
( f /. n = G * (i1,i2) & f /. (n + 1) = G * (j1,(j2 + 1)) ) by A2, A5, A9, A8, A16, A17, A22, A19, A27, A35, Th15, Th16;
then A38: 1 = (abs (i1 - j1)) + (abs (i2 - (j2 + 1))) by A1, A13, A29, A28, Def9
.= (abs (i1 - j1)) + (abs (- ((j2 + 1) - i2)))
.= (abs (i1 - j1)) + (abs ((j2 + 1) - i2)) by COMPLEX1:52 ;
0 < (j2 + 1) - i2 by A36, XREAL_1:50;
then A39: abs ((j2 + 1) - i2) = (j2 + 1) - i2 by ABSVALUE:def_1;
0 <= abs (i1 - j1) by COMPLEX1:46;
then 0 + ((j2 + 1) - i2) <= 1 by A38, A39, XREAL_1:7;
then (j2 + 1) - i2 = 1 by A37, XXREAL_0:1;
hence contradiction by A35; ::_thesis: verum
end;
case ( i <= i2 & i <= j2 ) ; ::_thesis: 1 = (abs (i1 - j1)) + (abs (i2 - j2))
then ( f /. n = G * (i1,(i2 + 1)) & f /. (n + 1) = G * (j1,(j2 + 1)) ) by A2, A5, A9, A10, A8, A16, A17, A22, A20, A27, Th16;
hence 1 = (abs (i1 - j1)) + (abs ((i2 + 1) - (j2 + 1))) by A1, A13, A21, A28, Def9
.= (abs (i1 - j1)) + (abs (i2 - j2)) ;
::_thesis: verum
end;
end;
end;
hence (abs (i1 - j1)) + (abs (i2 - j2)) = 1 ; ::_thesis: verum
end;
A40: 1 <= i by A2, FINSEQ_1:1;
A41: i <= width G by A2, FINSEQ_1:1;
now__::_thesis:_for_n_being_Element_of_NAT_st_n_in_dom_f_holds_
ex_m,_k_being_Element_of_NAT_st_
(_[m,k]_in_Indices_(DelCol_(G,i))_&_f_/._n_=_(DelCol_(G,i))_*_(m,k)_)
let n be Element of NAT ; ::_thesis: ( n in dom f implies ex m, k being Element of NAT st
( [m,k] in Indices (DelCol (G,i)) & f /. n = (DelCol (G,i)) * (m,k) ) )
assume A42: n in dom f ; ::_thesis: ex m, k being Element of NAT st
( [m,k] in Indices (DelCol (G,i)) & f /. n = (DelCol (G,i)) * (m,k) )
then consider m, k being Element of NAT such that
A43: [m,k] in Indices G and
A44: f /. n = G * (m,k) by A1, Def9;
take m = m; ::_thesis: ex k being Element of NAT st
( [m,k] in Indices (DelCol (G,i)) & f /. n = (DelCol (G,i)) * (m,k) )
A45: m in dom G by A7, A43, ZFMISC_1:87;
A46: k in Seg (width G) by A7, A43, ZFMISC_1:87;
then A47: 1 <= k by FINSEQ_1:1;
A48: k <= M + 1 by A9, A46, FINSEQ_1:1;
now__::_thesis:_ex_k_being_Element_of_NAT_st_
(_[m,k]_in_Indices_(DelCol_(G,i))_&_f_/._n_=_(DelCol_(G,i))_*_(m,k)_)
percases ( k < i or i <= k ) ;
supposeA49: k < i ; ::_thesis: ex k being Element of NAT st
( [m,k] in Indices (DelCol (G,i)) & f /. n = (DelCol (G,i)) * (m,k) )
take k = k; ::_thesis: ( [m,k] in Indices (DelCol (G,i)) & f /. n = (DelCol (G,i)) * (m,k) )
k < width G by A41, A49, XXREAL_0:2;
then k <= M by A9, NAT_1:13;
then k in Seg M by A47, FINSEQ_1:1;
hence ( [m,k] in Indices (DelCol (G,i)) & f /. n = (DelCol (G,i)) * (m,k) ) by A2, A5, A9, A10, A11, A8, A6, A44, A45, A47, A49, Th15, ZFMISC_1:87; ::_thesis: verum
end;
suppose i <= k ; ::_thesis: ex l being Element of NAT st
( [m,l] in Indices (DelCol (G,i)) & f /. n = (DelCol (G,i)) * (m,l) )
then A50: i < k by A3, A42, A44, A45, Th8, XXREAL_0:1;
then reconsider l = k - 1 as Element of NAT by A40, INT_1:5, XXREAL_0:2;
take l = l; ::_thesis: ( [m,l] in Indices (DelCol (G,i)) & f /. n = (DelCol (G,i)) * (m,l) )
A51: l <= M by A48, XREAL_1:20;
i + 1 <= k by A50, NAT_1:13;
then A52: i <= k - 1 by XREAL_1:19;
then 1 <= l by A40, XXREAL_0:2;
then A53: l in Seg M by A51, FINSEQ_1:1;
(DelCol (G,i)) * (m,l) = G * (m,(l + 1)) by A2, A9, A40, A45, A52, A51, Th16;
hence ( [m,l] in Indices (DelCol (G,i)) & f /. n = (DelCol (G,i)) * (m,l) ) by A5, A11, A8, A6, A44, A45, A53, ZFMISC_1:87; ::_thesis: verum
end;
end;
end;
hence ex k being Element of NAT st
( [m,k] in Indices (DelCol (G,i)) & f /. n = (DelCol (G,i)) * (m,k) ) ; ::_thesis: verum
end;
hence f is_sequence_on DelCol (G,i) by A12, Def9; ::_thesis: verum
end;
theorem Th26: :: GOBOARD1:26
for i being Element of NAT
for G being Go-board
for f being FinSequence of (TOP-REAL 2) st f is_sequence_on G & i in dom f holds
ex n being Element of NAT st
( n in dom G & f /. i in rng (Line (G,n)) )
proof
let i be Element of NAT ; ::_thesis: for G being Go-board
for f being FinSequence of (TOP-REAL 2) st f is_sequence_on G & i in dom f holds
ex n being Element of NAT st
( n in dom G & f /. i in rng (Line (G,n)) )
let G be Go-board; ::_thesis: for f being FinSequence of (TOP-REAL 2) st f is_sequence_on G & i in dom f holds
ex n being Element of NAT st
( n in dom G & f /. i in rng (Line (G,n)) )
let f be FinSequence of (TOP-REAL 2); ::_thesis: ( f is_sequence_on G & i in dom f implies ex n being Element of NAT st
( n in dom G & f /. i in rng (Line (G,n)) ) )
assume ( f is_sequence_on G & i in dom f ) ; ::_thesis: ex n being Element of NAT st
( n in dom G & f /. i in rng (Line (G,n)) )
then consider n, m being Element of NAT such that
A1: [n,m] in Indices G and
A2: f /. i = G * (n,m) by Def9;
set L = Line (G,n);
take n ; ::_thesis: ( n in dom G & f /. i in rng (Line (G,n)) )
A3: Indices G = [:(dom G),(Seg (width G)):] by MATRIX_1:def_4;
hence n in dom G by A1, ZFMISC_1:87; ::_thesis: f /. i in rng (Line (G,n))
A4: m in Seg (width G) by A1, A3, ZFMISC_1:87;
len (Line (G,n)) = width G by MATRIX_1:def_7;
then A5: m in dom (Line (G,n)) by A4, FINSEQ_1:def_3;
(Line (G,n)) . m = f /. i by A2, A4, MATRIX_1:def_7;
hence f /. i in rng (Line (G,n)) by A5, FUNCT_1:def_3; ::_thesis: verum
end;
theorem Th27: :: GOBOARD1:27
for i, n being Element of NAT
for G being Go-board
for f being FinSequence of (TOP-REAL 2) st f is_sequence_on G & i in dom f & i + 1 in dom f & n in dom G & f /. i in rng (Line (G,n)) & not f /. (i + 1) in rng (Line (G,n)) holds
for k being Element of NAT st f /. (i + 1) in rng (Line (G,k)) & k in dom G holds
abs (n - k) = 1
proof
let i, n be Element of NAT ; ::_thesis: for G being Go-board
for f being FinSequence of (TOP-REAL 2) st f is_sequence_on G & i in dom f & i + 1 in dom f & n in dom G & f /. i in rng (Line (G,n)) & not f /. (i + 1) in rng (Line (G,n)) holds
for k being Element of NAT st f /. (i + 1) in rng (Line (G,k)) & k in dom G holds
abs (n - k) = 1
let G be Go-board; ::_thesis: for f being FinSequence of (TOP-REAL 2) st f is_sequence_on G & i in dom f & i + 1 in dom f & n in dom G & f /. i in rng (Line (G,n)) & not f /. (i + 1) in rng (Line (G,n)) holds
for k being Element of NAT st f /. (i + 1) in rng (Line (G,k)) & k in dom G holds
abs (n - k) = 1
let f be FinSequence of (TOP-REAL 2); ::_thesis: ( f is_sequence_on G & i in dom f & i + 1 in dom f & n in dom G & f /. i in rng (Line (G,n)) & not f /. (i + 1) in rng (Line (G,n)) implies for k being Element of NAT st f /. (i + 1) in rng (Line (G,k)) & k in dom G holds
abs (n - k) = 1 )
assume that
A1: f is_sequence_on G and
A2: i in dom f and
A3: i + 1 in dom f and
A4: ( n in dom G & f /. i in rng (Line (G,n)) ) ; ::_thesis: ( f /. (i + 1) in rng (Line (G,n)) or for k being Element of NAT st f /. (i + 1) in rng (Line (G,k)) & k in dom G holds
abs (n - k) = 1 )
consider j1, j2 being Element of NAT such that
A5: [j1,j2] in Indices G and
A6: f /. (i + 1) = G * (j1,j2) by A1, A3, Def9;
A7: Indices G = [:(dom G),(Seg (width G)):] by MATRIX_1:def_4;
then A8: j1 in dom G by A5, ZFMISC_1:87;
consider i1, i2 being Element of NAT such that
A9: [i1,i2] in Indices G and
A10: f /. i = G * (i1,i2) by A1, A2, Def9;
A11: i2 in Seg (width G) by A9, A7, ZFMISC_1:87;
len (Line (G,i1)) = width G by MATRIX_1:def_7;
then A12: i2 in dom (Line (G,i1)) by A11, FINSEQ_1:def_3;
(Line (G,i1)) . i2 = f /. i by A10, A11, MATRIX_1:def_7;
then A13: f /. i in rng (Line (G,i1)) by A12, FUNCT_1:def_3;
i1 in dom G by A9, A7, ZFMISC_1:87;
then i1 = n by A4, A13, Th3;
then A14: (abs (n - j1)) + (abs (i2 - j2)) = 1 by A1, A2, A3, A9, A10, A5, A6, Def9;
A15: j2 in Seg (width G) by A5, A7, ZFMISC_1:87;
len (Line (G,j1)) = width G by MATRIX_1:def_7;
then A16: j2 in dom (Line (G,j1)) by A15, FINSEQ_1:def_3;
A17: (Line (G,j1)) . j2 = f /. (i + 1) by A6, A15, MATRIX_1:def_7;
then A18: f /. (i + 1) in rng (Line (G,j1)) by A16, FUNCT_1:def_3;
now__::_thesis:_(_f_/._(i_+_1)_in_rng_(Line_(G,n))_or_for_k_being_Element_of_NAT_st_f_/._(i_+_1)_in_rng_(Line_(G,k))_&_k_in_dom_G_holds_
abs_(n_-_k)_=_1_)
percases ( ( abs (n - j1) = 1 & i2 = j2 ) or ( abs (i2 - j2) = 1 & n = j1 ) ) by A14, SEQM_3:42;
suppose ( abs (n - j1) = 1 & i2 = j2 ) ; ::_thesis: ( f /. (i + 1) in rng (Line (G,n)) or for k being Element of NAT st f /. (i + 1) in rng (Line (G,k)) & k in dom G holds
abs (n - k) = 1 )
hence ( f /. (i + 1) in rng (Line (G,n)) or for k being Element of NAT st f /. (i + 1) in rng (Line (G,k)) & k in dom G holds
abs (n - k) = 1 ) by A8, A18, Th3; ::_thesis: verum
end;
suppose ( abs (i2 - j2) = 1 & n = j1 ) ; ::_thesis: ( f /. (i + 1) in rng (Line (G,n)) or for k being Element of NAT st f /. (i + 1) in rng (Line (G,k)) & k in dom G holds
abs (n - k) = 1 )
hence ( f /. (i + 1) in rng (Line (G,n)) or for k being Element of NAT st f /. (i + 1) in rng (Line (G,k)) & k in dom G holds
abs (n - k) = 1 ) by A17, A16, FUNCT_1:def_3; ::_thesis: verum
end;
end;
end;
hence ( f /. (i + 1) in rng (Line (G,n)) or for k being Element of NAT st f /. (i + 1) in rng (Line (G,k)) & k in dom G holds
abs (n - k) = 1 ) ; ::_thesis: verum
end;
theorem Th28: :: GOBOARD1:28
for i, m being Element of NAT
for G being Go-board
for f being FinSequence of (TOP-REAL 2) st 1 <= len f & f /. (len f) in rng (Line (G,(len G))) & f is_sequence_on G & i in dom G & i + 1 in dom G & m in dom f & f /. m in rng (Line (G,i)) & ( for k being Element of NAT st k in dom f & f /. k in rng (Line (G,i)) holds
k <= m ) holds
( m + 1 in dom f & f /. (m + 1) in rng (Line (G,(i + 1))) )
proof
let i, m be Element of NAT ; ::_thesis: for G being Go-board
for f being FinSequence of (TOP-REAL 2) st 1 <= len f & f /. (len f) in rng (Line (G,(len G))) & f is_sequence_on G & i in dom G & i + 1 in dom G & m in dom f & f /. m in rng (Line (G,i)) & ( for k being Element of NAT st k in dom f & f /. k in rng (Line (G,i)) holds
k <= m ) holds
( m + 1 in dom f & f /. (m + 1) in rng (Line (G,(i + 1))) )
let G be Go-board; ::_thesis: for f being FinSequence of (TOP-REAL 2) st 1 <= len f & f /. (len f) in rng (Line (G,(len G))) & f is_sequence_on G & i in dom G & i + 1 in dom G & m in dom f & f /. m in rng (Line (G,i)) & ( for k being Element of NAT st k in dom f & f /. k in rng (Line (G,i)) holds
k <= m ) holds
( m + 1 in dom f & f /. (m + 1) in rng (Line (G,(i + 1))) )
let f be FinSequence of (TOP-REAL 2); ::_thesis: ( 1 <= len f & f /. (len f) in rng (Line (G,(len G))) & f is_sequence_on G & i in dom G & i + 1 in dom G & m in dom f & f /. m in rng (Line (G,i)) & ( for k being Element of NAT st k in dom f & f /. k in rng (Line (G,i)) holds
k <= m ) implies ( m + 1 in dom f & f /. (m + 1) in rng (Line (G,(i + 1))) ) )
assume that
A1: 1 <= len f and
A2: f /. (len f) in rng (Line (G,(len G))) and
A3: f is_sequence_on G and
A4: i in dom G and
A5: i + 1 in dom G and
A6: m in dom f and
A7: f /. m in rng (Line (G,i)) and
A8: for k being Element of NAT st k in dom f & f /. k in rng (Line (G,i)) holds
k <= m ; ::_thesis: ( m + 1 in dom f & f /. (m + 1) in rng (Line (G,(i + 1))) )
reconsider p = f /. (len f), q = f /. m as Point of (TOP-REAL 2) ;
defpred S1[ Nat, set ] means ( $2 in dom G & ( for k being Element of NAT st k = $2 holds
f /. $1 in rng (Line (G,k)) ) );
A9: for n being Element of NAT st n in dom f holds
ex k being Element of NAT st
( k in dom G & f /. n in rng (Line (G,k)) )
proof
assume ex n being Element of NAT st
( n in dom f & ( for k being Element of NAT holds
( not k in dom G or not f /. n in rng (Line (G,k)) ) ) ) ; ::_thesis: contradiction
then consider n being Element of NAT such that
A10: n in dom f and
A11: for k being Element of NAT st k in dom G holds
not f /. n in rng (Line (G,k)) ;
consider i, j being Element of NAT such that
A12: [i,j] in Indices G and
A13: f /. n = G * (i,j) by A3, A10, Def9;
A14: [i,j] in [:(dom G),(Seg (width G)):] by A12, MATRIX_1:def_4;
then i in dom G by ZFMISC_1:87;
then A15: not f /. n in rng (Line (G,i)) by A11;
A16: j in Seg (width G) by A14, ZFMISC_1:87;
then j in Seg (len (Line (G,i))) by MATRIX_1:def_7;
then A17: j in dom (Line (G,i)) by FINSEQ_1:def_3;
(Line (G,i)) . j = G * (i,j) by A16, MATRIX_1:def_7;
hence contradiction by A13, A15, A17, FUNCT_1:def_3; ::_thesis: verum
end;
A18: for n being Nat st n in Seg (len f) holds
ex r being Real st S1[n,r]
proof
let n be Nat; ::_thesis: ( n in Seg (len f) implies ex r being Real st S1[n,r] )
assume n in Seg (len f) ; ::_thesis: ex r being Real st S1[n,r]
then n in dom f by FINSEQ_1:def_3;
then consider k being Element of NAT such that
A19: k in dom G and
A20: f /. n in rng (Line (G,k)) by A9;
take r = k; ::_thesis: S1[n,r]
thus r in dom G by A19; ::_thesis: for k being Element of NAT st k = r holds
f /. n in rng (Line (G,k))
let m be Element of NAT ; ::_thesis: ( m = r implies f /. n in rng (Line (G,m)) )
assume m = r ; ::_thesis: f /. n in rng (Line (G,m))
hence f /. n in rng (Line (G,m)) by A20; ::_thesis: verum
end;
consider v being FinSequence of REAL such that
A21: dom v = Seg (len f) and
A22: for n being Nat st n in Seg (len f) holds
S1[n,v . n] from FINSEQ_1:sch_5(A18);
A23: dom f = Seg (len f) by FINSEQ_1:def_3;
A24: for k being Element of NAT st k in dom v & v . k = i holds
k <= m
proof
let k be Element of NAT ; ::_thesis: ( k in dom v & v . k = i implies k <= m )
assume that
A25: k in dom v and
A26: v . k = i ; ::_thesis: k <= m
f /. k in rng (Line (G,i)) by A21, A22, A25, A26;
hence k <= m by A8, A21, A23, A25; ::_thesis: verum
end;
A27: rng v c= dom G
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng v or x in dom G )
assume x in rng v ; ::_thesis: x in dom G
then ex y being Nat st
( y in dom v & v . y = x ) by FINSEQ_2:10;
hence x in dom G by A21, A22; ::_thesis: verum
end;
A28: len v = len f by A21, FINSEQ_1:def_3;
A29: for k being Element of NAT st 1 <= k & k <= (len v) - 1 holds
for r, s being Real st r = v . k & s = v . (k + 1) & not abs (r - s) = 1 holds
r = s
proof
let k be Element of NAT ; ::_thesis: ( 1 <= k & k <= (len v) - 1 implies for r, s being Real st r = v . k & s = v . (k + 1) & not abs (r - s) = 1 holds
r = s )
assume that
A30: 1 <= k and
A31: k <= (len v) - 1 ; ::_thesis: for r, s being Real st r = v . k & s = v . (k + 1) & not abs (r - s) = 1 holds
r = s
A32: k + 1 <= len v by A31, XREAL_1:19;
let r, s be Real; ::_thesis: ( r = v . k & s = v . (k + 1) & not abs (r - s) = 1 implies r = s )
assume that
A33: r = v . k and
A34: s = v . (k + 1) ; ::_thesis: ( abs (r - s) = 1 or r = s )
1 <= k + 1 by NAT_1:11;
then A35: k + 1 in dom f by A28, A32, FINSEQ_3:25;
then A36: s in rng v by A21, A23, A34, FUNCT_1:def_3;
then A37: s in dom G by A27;
k <= k + 1 by NAT_1:11;
then k <= len f by A28, A32, XXREAL_0:2;
then A38: k in dom f by A30, FINSEQ_3:25;
then A39: r in rng v by A21, A23, A33, FUNCT_1:def_3;
then r in dom G by A27;
then reconsider n1 = r, n2 = s as Element of NAT by A37;
set L1 = Line (G,n1);
set L2 = Line (G,n2);
f /. k in rng (Line (G,n1)) by A22, A23, A38, A33;
then consider x being Nat such that
A40: x in dom (Line (G,n1)) and
A41: (Line (G,n1)) . x = f /. k by FINSEQ_2:10;
A42: ( dom (Line (G,n1)) = Seg (len (Line (G,n1))) & len (Line (G,n1)) = width G ) by FINSEQ_1:def_3, MATRIX_1:def_7;
then A43: f /. k = G * (n1,x) by A40, A41, MATRIX_1:def_7;
f /. (k + 1) in rng (Line (G,n2)) by A22, A23, A35, A34;
then consider y being Nat such that
A44: y in dom (Line (G,n2)) and
A45: (Line (G,n2)) . y = f /. (k + 1) by FINSEQ_2:10;
reconsider x = x, y = y as Element of NAT by ORDINAL1:def_12;
[n1,x] in [:(dom G),(Seg (width G)):] by A27, A39, A40, A42, ZFMISC_1:87;
then A46: [n1,x] in Indices G by MATRIX_1:def_4;
A47: ( Seg (len (Line (G,n2))) = dom (Line (G,n2)) & len (Line (G,n2)) = width G ) by FINSEQ_1:def_3, MATRIX_1:def_7;
then [n2,y] in [:(dom G),(Seg (width G)):] by A27, A36, A44, ZFMISC_1:87;
then A48: [n2,y] in Indices G by MATRIX_1:def_4;
f /. (k + 1) = G * (n2,y) by A47, A44, A45, MATRIX_1:def_7;
then (abs (n1 - n2)) + (abs (x - y)) = 1 by A3, A38, A35, A43, A46, A48, Def9;
hence ( abs (r - s) = 1 or r = s ) by SEQM_3:42; ::_thesis: verum
end;
A49: v . m = i
proof
A50: v . m in dom G by A6, A22, A23;
then reconsider k = v . m as Element of NAT ;
assume A51: v . m <> i ; ::_thesis: contradiction
q in rng (Line (G,k)) by A6, A22, A23;
hence contradiction by A4, A7, A51, A50, Th3; ::_thesis: verum
end;
( 1 <= m & m <= len f ) by A6, FINSEQ_3:25;
then 1 <= len f by XXREAL_0:2;
then A52: len f in dom f by FINSEQ_3:25;
A53: v . (len v) = len G
proof
0 < len G by Lm1;
then 0 + 1 <= len G by NAT_1:13;
then A54: len G in dom G by FINSEQ_3:25;
A55: v . (len v) in dom G by A22, A28, A23, A52;
then reconsider k = v . (len v) as Element of NAT ;
assume A56: v . (len v) <> len G ; ::_thesis: contradiction
p in rng (Line (G,k)) by A22, A28, A23, A52;
hence contradiction by A2, A56, A55, A54, Th3; ::_thesis: verum
end;
A57: ( dom G = Seg (len G) & v <> {} ) by A1, A21, FINSEQ_1:def_3;
hence m + 1 in dom f by A4, A5, A6, A21, A23, A27, A53, A29, A49, A24, SEQM_3:45; ::_thesis: f /. (m + 1) in rng (Line (G,(i + 1)))
( m + 1 in dom v & v . (m + 1) = i + 1 ) by A4, A5, A6, A21, A23, A57, A27, A53, A29, A49, A24, SEQM_3:45;
hence f /. (m + 1) in rng (Line (G,(i + 1))) by A21, A22; ::_thesis: verum
end;
theorem :: GOBOARD1:29
for G being Go-board
for f being FinSequence of (TOP-REAL 2) st 1 <= len f & f /. 1 in rng (Line (G,1)) & f /. (len f) in rng (Line (G,(len G))) & f is_sequence_on G holds
( ( for i being Element of NAT st 1 <= i & i <= len G holds
ex k being Element of NAT st
( k in dom f & f /. k in rng (Line (G,i)) ) ) & ( for i being Element of NAT st 1 <= i & i <= len G & 2 <= len f holds
L~ f meets rng (Line (G,i)) ) & ( for i, j, k, m being Element of NAT st 1 <= i & i <= len G & 1 <= j & j <= len G & k in dom f & m in dom f & f /. k in rng (Line (G,i)) & ( for n being Element of NAT st n in dom f & f /. n in rng (Line (G,i)) holds
n <= k ) & k < m & f /. m in rng (Line (G,j)) holds
i < j ) )
proof
let G be Go-board; ::_thesis: for f being FinSequence of (TOP-REAL 2) st 1 <= len f & f /. 1 in rng (Line (G,1)) & f /. (len f) in rng (Line (G,(len G))) & f is_sequence_on G holds
( ( for i being Element of NAT st 1 <= i & i <= len G holds
ex k being Element of NAT st
( k in dom f & f /. k in rng (Line (G,i)) ) ) & ( for i being Element of NAT st 1 <= i & i <= len G & 2 <= len f holds
L~ f meets rng (Line (G,i)) ) & ( for i, j, k, m being Element of NAT st 1 <= i & i <= len G & 1 <= j & j <= len G & k in dom f & m in dom f & f /. k in rng (Line (G,i)) & ( for n being Element of NAT st n in dom f & f /. n in rng (Line (G,i)) holds
n <= k ) & k < m & f /. m in rng (Line (G,j)) holds
i < j ) )
let f be FinSequence of (TOP-REAL 2); ::_thesis: ( 1 <= len f & f /. 1 in rng (Line (G,1)) & f /. (len f) in rng (Line (G,(len G))) & f is_sequence_on G implies ( ( for i being Element of NAT st 1 <= i & i <= len G holds
ex k being Element of NAT st
( k in dom f & f /. k in rng (Line (G,i)) ) ) & ( for i being Element of NAT st 1 <= i & i <= len G & 2 <= len f holds
L~ f meets rng (Line (G,i)) ) & ( for i, j, k, m being Element of NAT st 1 <= i & i <= len G & 1 <= j & j <= len G & k in dom f & m in dom f & f /. k in rng (Line (G,i)) & ( for n being Element of NAT st n in dom f & f /. n in rng (Line (G,i)) holds
n <= k ) & k < m & f /. m in rng (Line (G,j)) holds
i < j ) ) )
assume that
A1: 1 <= len f and
A2: f /. 1 in rng (Line (G,1)) and
A3: f /. (len f) in rng (Line (G,(len G))) and
A4: f is_sequence_on G ; ::_thesis: ( ( for i being Element of NAT st 1 <= i & i <= len G holds
ex k being Element of NAT st
( k in dom f & f /. k in rng (Line (G,i)) ) ) & ( for i being Element of NAT st 1 <= i & i <= len G & 2 <= len f holds
L~ f meets rng (Line (G,i)) ) & ( for i, j, k, m being Element of NAT st 1 <= i & i <= len G & 1 <= j & j <= len G & k in dom f & m in dom f & f /. k in rng (Line (G,i)) & ( for n being Element of NAT st n in dom f & f /. n in rng (Line (G,i)) holds
n <= k ) & k < m & f /. m in rng (Line (G,j)) holds
i < j ) )
A5: len f in dom f by A1, FINSEQ_3:25;
defpred S1[ Element of NAT ] means ( 1 <= $1 & $1 <= len G implies ex k being Element of NAT st
( k in dom f & f /. k in rng (Line (G,$1)) ) );
A6: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A7: ( 1 <= k & k <= len G implies ex i being Element of NAT st
( i in dom f & f /. i in rng (Line (G,k)) ) ) ; ::_thesis: S1[k + 1]
assume that
A8: 1 <= k + 1 and
A9: k + 1 <= len G ; ::_thesis: ex k being Element of NAT st
( k in dom f & f /. k in rng (Line (G,(k + 1))) )
A10: k + 1 in dom G by A8, A9, FINSEQ_3:25;
percases ( k = 0 or k <> 0 ) ;
supposeA11: k = 0 ; ::_thesis: ex k being Element of NAT st
( k in dom f & f /. k in rng (Line (G,(k + 1))) )
take 1 ; ::_thesis: ( 1 in dom f & f /. 1 in rng (Line (G,(k + 1))) )
thus ( 1 in dom f & f /. 1 in rng (Line (G,(k + 1))) ) by A1, A2, A11, FINSEQ_3:25; ::_thesis: verum
end;
supposeA12: k <> 0 ; ::_thesis: ex k being Element of NAT st
( k in dom f & f /. k in rng (Line (G,(k + 1))) )
defpred S2[ Nat] means ( $1 in dom f & f /. $1 in rng (Line (G,k)) );
A13: for i being Nat st S2[i] holds
i <= len f by FINSEQ_3:25;
A14: 0 + 1 <= k by A12, NAT_1:13;
then A15: ex i being Nat st S2[i] by A7, A9, NAT_1:13;
consider m being Nat such that
A16: ( S2[m] & ( for i being Nat st S2[i] holds
i <= m ) ) from NAT_1:sch_6(A13, A15);
take m + 1 ; ::_thesis: ( m + 1 in dom f & f /. (m + 1) in rng (Line (G,(k + 1))) )
k <= len G by A9, NAT_1:13;
then A17: k in dom G by A14, FINSEQ_3:25;
for i being Element of NAT st S2[i] holds
i <= m by A16;
hence ( m + 1 in dom f & f /. (m + 1) in rng (Line (G,(k + 1))) ) by A1, A3, A4, A10, A17, A16, Th28; ::_thesis: verum
end;
end;
end;
A18: S1[ 0 ] ;
thus A19: for i being Element of NAT holds S1[i] from NAT_1:sch_1(A18, A6); ::_thesis: ( ( for i being Element of NAT st 1 <= i & i <= len G & 2 <= len f holds
L~ f meets rng (Line (G,i)) ) & ( for i, j, k, m being Element of NAT st 1 <= i & i <= len G & 1 <= j & j <= len G & k in dom f & m in dom f & f /. k in rng (Line (G,i)) & ( for n being Element of NAT st n in dom f & f /. n in rng (Line (G,i)) holds
n <= k ) & k < m & f /. m in rng (Line (G,j)) holds
i < j ) )
thus for i being Element of NAT st 1 <= i & i <= len G & 2 <= len f holds
L~ f meets rng (Line (G,i)) ::_thesis: for i, j, k, m being Element of NAT st 1 <= i & i <= len G & 1 <= j & j <= len G & k in dom f & m in dom f & f /. k in rng (Line (G,i)) & ( for n being Element of NAT st n in dom f & f /. n in rng (Line (G,i)) holds
n <= k ) & k < m & f /. m in rng (Line (G,j)) holds
i < j
proof
let i be Element of NAT ; ::_thesis: ( 1 <= i & i <= len G & 2 <= len f implies L~ f meets rng (Line (G,i)) )
assume that
A20: ( 1 <= i & i <= len G ) and
A21: 2 <= len f ; ::_thesis: L~ f meets rng (Line (G,i))
consider k being Element of NAT such that
A22: k in dom f and
A23: f /. k in rng (Line (G,i)) by A19, A20;
f /. k in L~ f by A21, A22, Th1;
then (L~ f) /\ (rng (Line (G,i))) <> {} by A23, XBOOLE_0:def_4;
hence L~ f meets rng (Line (G,i)) by XBOOLE_0:def_7; ::_thesis: verum
end;
let m, k, i, j be Element of NAT ; ::_thesis: ( 1 <= m & m <= len G & 1 <= k & k <= len G & i in dom f & j in dom f & f /. i in rng (Line (G,m)) & ( for n being Element of NAT st n in dom f & f /. n in rng (Line (G,m)) holds
n <= i ) & i < j & f /. j in rng (Line (G,k)) implies m < k )
assume that
A24: 1 <= m and
A25: m <= len G and
A26: ( 1 <= k & k <= len G ) and
A27: i in dom f and
A28: j in dom f and
A29: f /. i in rng (Line (G,m)) and
A30: for n being Element of NAT st n in dom f & f /. n in rng (Line (G,m)) holds
n <= i and
A31: i < j and
A32: f /. j in rng (Line (G,k)) ; ::_thesis: m < k
A33: ( i <= len f & j <= len f ) by A27, A28, FINSEQ_3:25;
now__::_thesis:_(_(_m_=_len_G_&_contradiction_)_or_(_m_<>_len_G_&_m_<_k_)_)
percases ( m = len G or m <> len G ) ;
case m = len G ; ::_thesis: contradiction
then len f <= i by A3, A5, A30;
hence contradiction by A31, A33, XXREAL_0:1; ::_thesis: verum
end;
case m <> len G ; ::_thesis: m < k
then m < len G by A25, XXREAL_0:1;
then ( 1 <= m + 1 & m + 1 <= len G ) by NAT_1:11, NAT_1:13;
then A34: m + 1 in dom G by FINSEQ_3:25;
reconsider l = j - i as Element of NAT by A31, INT_1:5;
defpred S2[ set ] means for n, l being Element of NAT st n = $1 & n > 0 & i + n in dom f & f /. (i + n) in rng (Line (G,l)) & l in dom G holds
m < l;
A35: k in dom G by A26, FINSEQ_3:25;
m in dom G by A24, A25, FINSEQ_3:25;
then A36: f /. (i + 1) in rng (Line (G,(m + 1))) by A1, A3, A4, A27, A29, A30, A34, Th28;
A37: for o being Element of NAT st S2[o] holds
S2[o + 1]
proof
let o be Element of NAT ; ::_thesis: ( S2[o] implies S2[o + 1] )
assume A38: S2[o] ; ::_thesis: S2[o + 1]
let n, l be Element of NAT ; ::_thesis: ( n = o + 1 & n > 0 & i + n in dom f & f /. (i + n) in rng (Line (G,l)) & l in dom G implies m < l )
assume that
A39: n = o + 1 and
A40: n > 0 and
A41: i + n in dom f and
A42: f /. (i + n) in rng (Line (G,l)) and
A43: l in dom G ; ::_thesis: m < l
now__::_thesis:_m_<_l
percases ( o = 0 or o <> 0 ) ;
suppose o = 0 ; ::_thesis: m < l
then l = m + 1 by A34, A36, A39, A42, A43, Th3;
hence m < l by NAT_1:13; ::_thesis: verum
end;
supposeA44: o <> 0 ; ::_thesis: m < l
1 <= i by A27, FINSEQ_3:25;
then A45: 1 <= i + o by NAT_1:12;
( i + n <= len f & i + o <= (i + o) + 1 ) by A41, FINSEQ_3:25, NAT_1:12;
then i + o <= len f by A39, XXREAL_0:2;
then A46: i + o in dom f by A45, FINSEQ_3:25;
then consider l1 being Element of NAT such that
A47: l1 in dom G and
A48: f /. (i + o) in rng (Line (G,l1)) by A4, Th26;
A49: m < l1 by A38, A44, A46, A47, A48;
A50: i + n = (i + o) + 1 by A39;
now__::_thesis:_m_<_l
percases ( f /. (i + n) in rng (Line (G,l1)) or for k being Element of NAT st f /. (i + n) in rng (Line (G,k)) & k in dom G holds
abs (l1 - k) = 1 ) by A4, A41, A50, A46, A47, A48, Th27;
suppose f /. (i + n) in rng (Line (G,l1)) ; ::_thesis: m < l
hence m < l by A42, A43, A47, A49, Th3; ::_thesis: verum
end;
suppose for k being Element of NAT st f /. (i + n) in rng (Line (G,k)) & k in dom G holds
abs (l1 - k) = 1 ; ::_thesis: m < l
then A51: abs (l1 - l) = 1 by A42, A43;
now__::_thesis:_m_<_l
percases ( ( l1 > l & l1 = l + 1 ) or ( l1 < l & l = l1 + 1 ) ) by A51, SEQM_3:41;
suppose ( l1 > l & l1 = l + 1 ) ; ::_thesis: m < l
then A52: m <= l by A49, NAT_1:13;
now__::_thesis:_(_(_m_=_l_&_contradiction_)_or_(_m_<_l_&_m_<_l_)_)
percases ( m = l or m < l ) by A52, XXREAL_0:1;
case m = l ; ::_thesis: contradiction
then i + n <= i by A30, A41, A42;
then n <= i - i by XREAL_1:19;
hence contradiction by A40; ::_thesis: verum
end;
case m < l ; ::_thesis: m < l
hence m < l ; ::_thesis: verum
end;
end;
end;
hence m < l ; ::_thesis: verum
end;
suppose ( l1 < l & l = l1 + 1 ) ; ::_thesis: m < l
hence m < l by A49, XXREAL_0:2; ::_thesis: verum
end;
end;
end;
hence m < l ; ::_thesis: verum
end;
end;
end;
hence m < l ; ::_thesis: verum
end;
end;
end;
hence m < l ; ::_thesis: verum
end;
A53: S2[ 0 ] ;
A54: for o being Element of NAT holds S2[o] from NAT_1:sch_1(A53, A37);
( 0 < j - i & i + l = j ) by A31, XREAL_1:50;
hence m < k by A28, A32, A54, A35; ::_thesis: verum
end;
end;
end;
hence m < k ; ::_thesis: verum
end;
theorem Th30: :: GOBOARD1:30
for i being Element of NAT
for G being Go-board
for f being FinSequence of (TOP-REAL 2) st f is_sequence_on G & i in dom f holds
ex n being Element of NAT st
( n in Seg (width G) & f /. i in rng (Col (G,n)) )
proof
let i be Element of NAT ; ::_thesis: for G being Go-board
for f being FinSequence of (TOP-REAL 2) st f is_sequence_on G & i in dom f holds
ex n being Element of NAT st
( n in Seg (width G) & f /. i in rng (Col (G,n)) )
let G be Go-board; ::_thesis: for f being FinSequence of (TOP-REAL 2) st f is_sequence_on G & i in dom f holds
ex n being Element of NAT st
( n in Seg (width G) & f /. i in rng (Col (G,n)) )
let f be FinSequence of (TOP-REAL 2); ::_thesis: ( f is_sequence_on G & i in dom f implies ex n being Element of NAT st
( n in Seg (width G) & f /. i in rng (Col (G,n)) ) )
assume ( f is_sequence_on G & i in dom f ) ; ::_thesis: ex n being Element of NAT st
( n in Seg (width G) & f /. i in rng (Col (G,n)) )
then consider n, m being Element of NAT such that
A1: [n,m] in Indices G and
A2: f /. i = G * (n,m) by Def9;
set L = Col (G,m);
take m ; ::_thesis: ( m in Seg (width G) & f /. i in rng (Col (G,m)) )
A3: Indices G = [:(dom G),(Seg (width G)):] by MATRIX_1:def_4;
hence m in Seg (width G) by A1, ZFMISC_1:87; ::_thesis: f /. i in rng (Col (G,m))
A4: n in dom G by A1, A3, ZFMISC_1:87;
len (Col (G,m)) = len G by MATRIX_1:def_8;
then A5: n in dom (Col (G,m)) by A4, FINSEQ_3:29;
(Col (G,m)) . n = f /. i by A2, A4, MATRIX_1:def_8;
hence f /. i in rng (Col (G,m)) by A5, FUNCT_1:def_3; ::_thesis: verum
end;
theorem Th31: :: GOBOARD1:31
for i, n being Element of NAT
for G being Go-board
for f being FinSequence of (TOP-REAL 2) st f is_sequence_on G & i in dom f & i + 1 in dom f & n in Seg (width G) & f /. i in rng (Col (G,n)) & not f /. (i + 1) in rng (Col (G,n)) holds
for k being Element of NAT st f /. (i + 1) in rng (Col (G,k)) & k in Seg (width G) holds
abs (n - k) = 1
proof
let i, n be Element of NAT ; ::_thesis: for G being Go-board
for f being FinSequence of (TOP-REAL 2) st f is_sequence_on G & i in dom f & i + 1 in dom f & n in Seg (width G) & f /. i in rng (Col (G,n)) & not f /. (i + 1) in rng (Col (G,n)) holds
for k being Element of NAT st f /. (i + 1) in rng (Col (G,k)) & k in Seg (width G) holds
abs (n - k) = 1
let G be Go-board; ::_thesis: for f being FinSequence of (TOP-REAL 2) st f is_sequence_on G & i in dom f & i + 1 in dom f & n in Seg (width G) & f /. i in rng (Col (G,n)) & not f /. (i + 1) in rng (Col (G,n)) holds
for k being Element of NAT st f /. (i + 1) in rng (Col (G,k)) & k in Seg (width G) holds
abs (n - k) = 1
let f be FinSequence of (TOP-REAL 2); ::_thesis: ( f is_sequence_on G & i in dom f & i + 1 in dom f & n in Seg (width G) & f /. i in rng (Col (G,n)) & not f /. (i + 1) in rng (Col (G,n)) implies for k being Element of NAT st f /. (i + 1) in rng (Col (G,k)) & k in Seg (width G) holds
abs (n - k) = 1 )
assume that
A1: f is_sequence_on G and
A2: i in dom f and
A3: i + 1 in dom f and
A4: ( n in Seg (width G) & f /. i in rng (Col (G,n)) ) ; ::_thesis: ( f /. (i + 1) in rng (Col (G,n)) or for k being Element of NAT st f /. (i + 1) in rng (Col (G,k)) & k in Seg (width G) holds
abs (n - k) = 1 )
consider j1, j2 being Element of NAT such that
A5: [j1,j2] in Indices G and
A6: f /. (i + 1) = G * (j1,j2) by A1, A3, Def9;
A7: Indices G = [:(dom G),(Seg (width G)):] by MATRIX_1:def_4;
then A8: j1 in dom G by A5, ZFMISC_1:87;
A9: j2 in Seg (width G) by A5, A7, ZFMISC_1:87;
len (Col (G,j2)) = len G by MATRIX_1:def_8;
then A10: j1 in dom (Col (G,j2)) by A8, FINSEQ_3:29;
consider i1, i2 being Element of NAT such that
A11: [i1,i2] in Indices G and
A12: f /. i = G * (i1,i2) by A1, A2, Def9;
A13: i1 in dom G by A11, A7, ZFMISC_1:87;
len (Col (G,i2)) = len G by MATRIX_1:def_8;
then A14: i1 in dom (Col (G,i2)) by A13, FINSEQ_3:29;
(Col (G,i2)) . i1 = f /. i by A12, A13, MATRIX_1:def_8;
then A15: f /. i in rng (Col (G,i2)) by A14, FUNCT_1:def_3;
i2 in Seg (width G) by A11, A7, ZFMISC_1:87;
then i2 = n by A4, A15, Th4;
then A16: (abs (i1 - j1)) + (abs (n - j2)) = 1 by A1, A2, A3, A11, A12, A5, A6, Def9;
A17: (Col (G,j2)) . j1 = f /. (i + 1) by A6, A8, MATRIX_1:def_8;
then A18: f /. (i + 1) in rng (Col (G,j2)) by A10, FUNCT_1:def_3;
now__::_thesis:_(_f_/._(i_+_1)_in_rng_(Col_(G,n))_or_for_k_being_Element_of_NAT_st_f_/._(i_+_1)_in_rng_(Col_(G,k))_&_k_in_Seg_(width_G)_holds_
abs_(n_-_k)_=_1_)
percases ( ( abs (i1 - j1) = 1 & n = j2 ) or ( abs (n - j2) = 1 & i1 = j1 ) ) by A16, SEQM_3:42;
suppose ( abs (i1 - j1) = 1 & n = j2 ) ; ::_thesis: ( f /. (i + 1) in rng (Col (G,n)) or for k being Element of NAT st f /. (i + 1) in rng (Col (G,k)) & k in Seg (width G) holds
abs (n - k) = 1 )
hence ( f /. (i + 1) in rng (Col (G,n)) or for k being Element of NAT st f /. (i + 1) in rng (Col (G,k)) & k in Seg (width G) holds
abs (n - k) = 1 ) by A17, A10, FUNCT_1:def_3; ::_thesis: verum
end;
suppose ( abs (n - j2) = 1 & i1 = j1 ) ; ::_thesis: ( f /. (i + 1) in rng (Col (G,n)) or for k being Element of NAT st f /. (i + 1) in rng (Col (G,k)) & k in Seg (width G) holds
abs (n - k) = 1 )
hence ( f /. (i + 1) in rng (Col (G,n)) or for k being Element of NAT st f /. (i + 1) in rng (Col (G,k)) & k in Seg (width G) holds
abs (n - k) = 1 ) by A9, A18, Th4; ::_thesis: verum
end;
end;
end;
hence ( f /. (i + 1) in rng (Col (G,n)) or for k being Element of NAT st f /. (i + 1) in rng (Col (G,k)) & k in Seg (width G) holds
abs (n - k) = 1 ) ; ::_thesis: verum
end;
theorem Th32: :: GOBOARD1:32
for i, m being Element of NAT
for G being Go-board
for f being FinSequence of (TOP-REAL 2) st 1 <= len f & f /. (len f) in rng (Col (G,(width G))) & f is_sequence_on G & i in Seg (width G) & i + 1 in Seg (width G) & m in dom f & f /. m in rng (Col (G,i)) & ( for k being Element of NAT st k in dom f & f /. k in rng (Col (G,i)) holds
k <= m ) holds
( m + 1 in dom f & f /. (m + 1) in rng (Col (G,(i + 1))) )
proof
let i, m be Element of NAT ; ::_thesis: for G being Go-board
for f being FinSequence of (TOP-REAL 2) st 1 <= len f & f /. (len f) in rng (Col (G,(width G))) & f is_sequence_on G & i in Seg (width G) & i + 1 in Seg (width G) & m in dom f & f /. m in rng (Col (G,i)) & ( for k being Element of NAT st k in dom f & f /. k in rng (Col (G,i)) holds
k <= m ) holds
( m + 1 in dom f & f /. (m + 1) in rng (Col (G,(i + 1))) )
let G be Go-board; ::_thesis: for f being FinSequence of (TOP-REAL 2) st 1 <= len f & f /. (len f) in rng (Col (G,(width G))) & f is_sequence_on G & i in Seg (width G) & i + 1 in Seg (width G) & m in dom f & f /. m in rng (Col (G,i)) & ( for k being Element of NAT st k in dom f & f /. k in rng (Col (G,i)) holds
k <= m ) holds
( m + 1 in dom f & f /. (m + 1) in rng (Col (G,(i + 1))) )
let f be FinSequence of (TOP-REAL 2); ::_thesis: ( 1 <= len f & f /. (len f) in rng (Col (G,(width G))) & f is_sequence_on G & i in Seg (width G) & i + 1 in Seg (width G) & m in dom f & f /. m in rng (Col (G,i)) & ( for k being Element of NAT st k in dom f & f /. k in rng (Col (G,i)) holds
k <= m ) implies ( m + 1 in dom f & f /. (m + 1) in rng (Col (G,(i + 1))) ) )
assume that
A1: 1 <= len f and
A2: f /. (len f) in rng (Col (G,(width G))) and
A3: f is_sequence_on G and
A4: i in Seg (width G) and
A5: i + 1 in Seg (width G) and
A6: m in dom f and
A7: f /. m in rng (Col (G,i)) and
A8: for k being Element of NAT st k in dom f & f /. k in rng (Col (G,i)) holds
k <= m ; ::_thesis: ( m + 1 in dom f & f /. (m + 1) in rng (Col (G,(i + 1))) )
defpred S1[ Nat, set ] means ( $2 in Seg (width G) & ( for k being Element of NAT st k = $2 holds
f /. $1 in rng (Col (G,k)) ) );
A9: dom G = Seg (len G) by FINSEQ_1:def_3;
A10: for n being Element of NAT st n in dom f holds
ex k being Element of NAT st
( k in Seg (width G) & f /. n in rng (Col (G,k)) )
proof
assume ex n being Element of NAT st
( n in dom f & ( for k being Element of NAT holds
( not k in Seg (width G) or not f /. n in rng (Col (G,k)) ) ) ) ; ::_thesis: contradiction
then consider n being Element of NAT such that
A11: n in dom f and
A12: for k being Element of NAT st k in Seg (width G) holds
not f /. n in rng (Col (G,k)) ;
consider i, j being Element of NAT such that
A13: [i,j] in Indices G and
A14: f /. n = G * (i,j) by A3, A11, Def9;
A15: [i,j] in [:(dom G),(Seg (width G)):] by A13, MATRIX_1:def_4;
then j in Seg (width G) by ZFMISC_1:87;
then A16: not f /. n in rng (Col (G,j)) by A12;
A17: i in dom G by A15, ZFMISC_1:87;
then i in Seg (len (Col (G,j))) by A9, MATRIX_1:def_8;
then A18: i in dom (Col (G,j)) by FINSEQ_1:def_3;
(Col (G,j)) . i = G * (i,j) by A17, MATRIX_1:def_8;
hence contradiction by A14, A16, A18, FUNCT_1:def_3; ::_thesis: verum
end;
A19: for n being Nat st n in Seg (len f) holds
ex r being Real st S1[n,r]
proof
let n be Nat; ::_thesis: ( n in Seg (len f) implies ex r being Real st S1[n,r] )
assume n in Seg (len f) ; ::_thesis: ex r being Real st S1[n,r]
then n in dom f by FINSEQ_1:def_3;
then consider k being Element of NAT such that
A20: k in Seg (width G) and
A21: f /. n in rng (Col (G,k)) by A10;
take r = k; ::_thesis: S1[n,r]
thus r in Seg (width G) by A20; ::_thesis: for k being Element of NAT st k = r holds
f /. n in rng (Col (G,k))
let m be Element of NAT ; ::_thesis: ( m = r implies f /. n in rng (Col (G,m)) )
assume m = r ; ::_thesis: f /. n in rng (Col (G,m))
hence f /. n in rng (Col (G,m)) by A21; ::_thesis: verum
end;
consider v being FinSequence of REAL such that
A22: dom v = Seg (len f) and
A23: for n being Nat st n in Seg (len f) holds
S1[n,v . n] from FINSEQ_1:sch_5(A19);
A24: dom f = Seg (len f) by FINSEQ_1:def_3;
A25: for k being Element of NAT st k in dom v & v . k = i holds
k <= m
proof
let k be Element of NAT ; ::_thesis: ( k in dom v & v . k = i implies k <= m )
assume that
A26: k in dom v and
A27: v . k = i ; ::_thesis: k <= m
f /. k in rng (Col (G,i)) by A22, A23, A26, A27;
hence k <= m by A8, A22, A24, A26; ::_thesis: verum
end;
A28: rng v c= Seg (width G)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng v or x in Seg (width G) )
assume x in rng v ; ::_thesis: x in Seg (width G)
then ex y being Nat st
( y in dom v & v . y = x ) by FINSEQ_2:10;
hence x in Seg (width G) by A22, A23; ::_thesis: verum
end;
A29: len v = len f by A22, FINSEQ_1:def_3;
A30: for k being Element of NAT st 1 <= k & k <= (len v) - 1 holds
for r, s being Real st r = v . k & s = v . (k + 1) & not abs (r - s) = 1 holds
r = s
proof
let k be Element of NAT ; ::_thesis: ( 1 <= k & k <= (len v) - 1 implies for r, s being Real st r = v . k & s = v . (k + 1) & not abs (r - s) = 1 holds
r = s )
assume that
A31: 1 <= k and
A32: k <= (len v) - 1 ; ::_thesis: for r, s being Real st r = v . k & s = v . (k + 1) & not abs (r - s) = 1 holds
r = s
A33: k + 1 <= len v by A32, XREAL_1:19;
let r, s be Real; ::_thesis: ( r = v . k & s = v . (k + 1) & not abs (r - s) = 1 implies r = s )
assume that
A34: r = v . k and
A35: s = v . (k + 1) ; ::_thesis: ( abs (r - s) = 1 or r = s )
1 <= k + 1 by NAT_1:11;
then A36: k + 1 in dom f by A29, A33, FINSEQ_3:25;
then A37: s in rng v by A22, A24, A35, FUNCT_1:def_3;
then A38: s in Seg (width G) by A28;
k <= k + 1 by NAT_1:11;
then k <= len f by A29, A33, XXREAL_0:2;
then A39: k in dom f by A31, FINSEQ_3:25;
then A40: r in rng v by A22, A24, A34, FUNCT_1:def_3;
then r in Seg (width G) by A28;
then reconsider n1 = r, n2 = s as Element of NAT by A38;
set L1 = Col (G,n1);
set L2 = Col (G,n2);
f /. k in rng (Col (G,n1)) by A23, A24, A39, A34;
then consider x being Nat such that
A41: x in dom (Col (G,n1)) and
A42: (Col (G,n1)) . x = f /. k by FINSEQ_2:10;
A43: ( dom (Col (G,n1)) = Seg (len (Col (G,n1))) & len (Col (G,n1)) = len G ) by FINSEQ_1:def_3, MATRIX_1:def_8;
then A44: f /. k = G * (x,n1) by A9, A41, A42, MATRIX_1:def_8;
f /. (k + 1) in rng (Col (G,n2)) by A23, A24, A36, A35;
then consider y being Nat such that
A45: y in dom (Col (G,n2)) and
A46: (Col (G,n2)) . y = f /. (k + 1) by FINSEQ_2:10;
reconsider x = x, y = y as Element of NAT by ORDINAL1:def_12;
[x,n1] in [:(dom G),(Seg (width G)):] by A9, A28, A40, A41, A43, ZFMISC_1:87;
then A47: [x,n1] in Indices G by MATRIX_1:def_4;
A48: ( dom (Col (G,n2)) = Seg (len (Col (G,n2))) & len (Col (G,n2)) = len G ) by FINSEQ_1:def_3, MATRIX_1:def_8;
then [y,n2] in [:(dom G),(Seg (width G)):] by A9, A28, A37, A45, ZFMISC_1:87;
then A49: [y,n2] in Indices G by MATRIX_1:def_4;
f /. (k + 1) = G * (y,n2) by A9, A48, A45, A46, MATRIX_1:def_8;
then (abs (x - y)) + (abs (n1 - n2)) = 1 by A3, A39, A36, A44, A47, A49, Def9;
hence ( abs (r - s) = 1 or r = s ) by SEQM_3:42; ::_thesis: verum
end;
A50: v . m = i
proof
A51: v . m in Seg (width G) by A6, A23, A24;
then reconsider k = v . m as Element of NAT ;
assume A52: v . m <> i ; ::_thesis: contradiction
f /. m in rng (Col (G,k)) by A6, A23, A24;
hence contradiction by A4, A7, A52, A51, Th4; ::_thesis: verum
end;
( 1 <= m & m <= len f ) by A6, FINSEQ_3:25;
then 1 <= len f by XXREAL_0:2;
then A53: len f in dom f by FINSEQ_3:25;
A54: v . (len v) = width G
proof
0 < width G by Lm1;
then 0 + 1 <= width G by NAT_1:13;
then A55: width G in Seg (width G) by FINSEQ_1:1;
A56: v . (len v) in Seg (width G) by A23, A29, A24, A53;
then reconsider k = v . (len v) as Element of NAT ;
assume A57: v . (len v) <> width G ; ::_thesis: contradiction
f /. (len f) in rng (Col (G,k)) by A23, A29, A24, A53;
hence contradiction by A2, A57, A56, A55, Th4; ::_thesis: verum
end;
A58: v <> {} by A1, A22;
hence m + 1 in dom f by A4, A5, A6, A22, A24, A28, A54, A30, A50, A25, SEQM_3:45; ::_thesis: f /. (m + 1) in rng (Col (G,(i + 1)))
( m + 1 in dom v & v . (m + 1) = i + 1 ) by A4, A5, A6, A22, A24, A58, A28, A54, A30, A50, A25, SEQM_3:45;
hence f /. (m + 1) in rng (Col (G,(i + 1))) by A22, A23; ::_thesis: verum
end;
theorem Th33: :: GOBOARD1:33
for G being Go-board
for f being FinSequence of (TOP-REAL 2) st 1 <= len f & f /. 1 in rng (Col (G,1)) & f /. (len f) in rng (Col (G,(width G))) & f is_sequence_on G holds
( ( for i being Element of NAT st 1 <= i & i <= width G holds
ex k being Element of NAT st
( k in dom f & f /. k in rng (Col (G,i)) ) ) & ( for i being Element of NAT st 1 <= i & i <= width G & 2 <= len f holds
L~ f meets rng (Col (G,i)) ) & ( for i, j, k, m being Element of NAT st 1 <= i & i <= width G & 1 <= j & j <= width G & k in dom f & m in dom f & f /. k in rng (Col (G,i)) & ( for n being Element of NAT st n in dom f & f /. n in rng (Col (G,i)) holds
n <= k ) & k < m & f /. m in rng (Col (G,j)) holds
i < j ) )
proof
let G be Go-board; ::_thesis: for f being FinSequence of (TOP-REAL 2) st 1 <= len f & f /. 1 in rng (Col (G,1)) & f /. (len f) in rng (Col (G,(width G))) & f is_sequence_on G holds
( ( for i being Element of NAT st 1 <= i & i <= width G holds
ex k being Element of NAT st
( k in dom f & f /. k in rng (Col (G,i)) ) ) & ( for i being Element of NAT st 1 <= i & i <= width G & 2 <= len f holds
L~ f meets rng (Col (G,i)) ) & ( for i, j, k, m being Element of NAT st 1 <= i & i <= width G & 1 <= j & j <= width G & k in dom f & m in dom f & f /. k in rng (Col (G,i)) & ( for n being Element of NAT st n in dom f & f /. n in rng (Col (G,i)) holds
n <= k ) & k < m & f /. m in rng (Col (G,j)) holds
i < j ) )
let f be FinSequence of (TOP-REAL 2); ::_thesis: ( 1 <= len f & f /. 1 in rng (Col (G,1)) & f /. (len f) in rng (Col (G,(width G))) & f is_sequence_on G implies ( ( for i being Element of NAT st 1 <= i & i <= width G holds
ex k being Element of NAT st
( k in dom f & f /. k in rng (Col (G,i)) ) ) & ( for i being Element of NAT st 1 <= i & i <= width G & 2 <= len f holds
L~ f meets rng (Col (G,i)) ) & ( for i, j, k, m being Element of NAT st 1 <= i & i <= width G & 1 <= j & j <= width G & k in dom f & m in dom f & f /. k in rng (Col (G,i)) & ( for n being Element of NAT st n in dom f & f /. n in rng (Col (G,i)) holds
n <= k ) & k < m & f /. m in rng (Col (G,j)) holds
i < j ) ) )
assume that
A1: 1 <= len f and
A2: f /. 1 in rng (Col (G,1)) and
A3: f /. (len f) in rng (Col (G,(width G))) and
A4: f is_sequence_on G ; ::_thesis: ( ( for i being Element of NAT st 1 <= i & i <= width G holds
ex k being Element of NAT st
( k in dom f & f /. k in rng (Col (G,i)) ) ) & ( for i being Element of NAT st 1 <= i & i <= width G & 2 <= len f holds
L~ f meets rng (Col (G,i)) ) & ( for i, j, k, m being Element of NAT st 1 <= i & i <= width G & 1 <= j & j <= width G & k in dom f & m in dom f & f /. k in rng (Col (G,i)) & ( for n being Element of NAT st n in dom f & f /. n in rng (Col (G,i)) holds
n <= k ) & k < m & f /. m in rng (Col (G,j)) holds
i < j ) )
A5: len f in dom f by A1, FINSEQ_3:25;
defpred S1[ Element of NAT ] means ( 1 <= $1 & $1 <= width G implies ex k being Element of NAT st
( k in dom f & f /. k in rng (Col (G,$1)) ) );
A6: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A7: ( 1 <= k & k <= width G implies ex i being Element of NAT st
( i in dom f & f /. i in rng (Col (G,k)) ) ) ; ::_thesis: S1[k + 1]
assume that
A8: 1 <= k + 1 and
A9: k + 1 <= width G ; ::_thesis: ex k being Element of NAT st
( k in dom f & f /. k in rng (Col (G,(k + 1))) )
A10: k + 1 in Seg (width G) by A8, A9, FINSEQ_1:1;
percases ( k = 0 or k <> 0 ) ;
supposeA11: k = 0 ; ::_thesis: ex k being Element of NAT st
( k in dom f & f /. k in rng (Col (G,(k + 1))) )
take 1 ; ::_thesis: ( 1 in dom f & f /. 1 in rng (Col (G,(k + 1))) )
thus ( 1 in dom f & f /. 1 in rng (Col (G,(k + 1))) ) by A1, A2, A11, FINSEQ_3:25; ::_thesis: verum
end;
supposeA12: k <> 0 ; ::_thesis: ex k being Element of NAT st
( k in dom f & f /. k in rng (Col (G,(k + 1))) )
defpred S2[ Nat] means ( $1 in dom f & f /. $1 in rng (Col (G,k)) );
A13: for i being Nat st S2[i] holds
i <= len f by FINSEQ_3:25;
A14: 0 + 1 <= k by A12, NAT_1:13;
then A15: ex i being Nat st S2[i] by A7, A9, NAT_1:13;
consider m being Nat such that
A16: ( S2[m] & ( for i being Nat st S2[i] holds
i <= m ) ) from NAT_1:sch_6(A13, A15);
take m + 1 ; ::_thesis: ( m + 1 in dom f & f /. (m + 1) in rng (Col (G,(k + 1))) )
k <= width G by A9, NAT_1:13;
then A17: k in Seg (width G) by A14, FINSEQ_1:1;
for i being Element of NAT st S2[i] holds
i <= m by A16;
hence ( m + 1 in dom f & f /. (m + 1) in rng (Col (G,(k + 1))) ) by A1, A3, A4, A10, A17, A16, Th32; ::_thesis: verum
end;
end;
end;
A18: S1[ 0 ] ;
thus A19: for i being Element of NAT holds S1[i] from NAT_1:sch_1(A18, A6); ::_thesis: ( ( for i being Element of NAT st 1 <= i & i <= width G & 2 <= len f holds
L~ f meets rng (Col (G,i)) ) & ( for i, j, k, m being Element of NAT st 1 <= i & i <= width G & 1 <= j & j <= width G & k in dom f & m in dom f & f /. k in rng (Col (G,i)) & ( for n being Element of NAT st n in dom f & f /. n in rng (Col (G,i)) holds
n <= k ) & k < m & f /. m in rng (Col (G,j)) holds
i < j ) )
thus for i being Element of NAT st 1 <= i & i <= width G & 2 <= len f holds
L~ f meets rng (Col (G,i)) ::_thesis: for i, j, k, m being Element of NAT st 1 <= i & i <= width G & 1 <= j & j <= width G & k in dom f & m in dom f & f /. k in rng (Col (G,i)) & ( for n being Element of NAT st n in dom f & f /. n in rng (Col (G,i)) holds
n <= k ) & k < m & f /. m in rng (Col (G,j)) holds
i < j
proof
let i be Element of NAT ; ::_thesis: ( 1 <= i & i <= width G & 2 <= len f implies L~ f meets rng (Col (G,i)) )
assume that
A20: ( 1 <= i & i <= width G ) and
A21: 2 <= len f ; ::_thesis: L~ f meets rng (Col (G,i))
consider k being Element of NAT such that
A22: k in dom f and
A23: f /. k in rng (Col (G,i)) by A19, A20;
f /. k in L~ f by A21, A22, Th1;
then (L~ f) /\ (rng (Col (G,i))) <> {} by A23, XBOOLE_0:def_4;
hence L~ f meets rng (Col (G,i)) by XBOOLE_0:def_7; ::_thesis: verum
end;
let m, k, i, j be Element of NAT ; ::_thesis: ( 1 <= m & m <= width G & 1 <= k & k <= width G & i in dom f & j in dom f & f /. i in rng (Col (G,m)) & ( for n being Element of NAT st n in dom f & f /. n in rng (Col (G,m)) holds
n <= i ) & i < j & f /. j in rng (Col (G,k)) implies m < k )
assume that
A24: 1 <= m and
A25: m <= width G and
A26: ( 1 <= k & k <= width G ) and
A27: i in dom f and
A28: j in dom f and
A29: f /. i in rng (Col (G,m)) and
A30: for n being Element of NAT st n in dom f & f /. n in rng (Col (G,m)) holds
n <= i and
A31: i < j and
A32: f /. j in rng (Col (G,k)) ; ::_thesis: m < k
A33: ( i <= len f & j <= len f ) by A27, A28, FINSEQ_3:25;
now__::_thesis:_(_(_m_=_width_G_&_contradiction_)_or_(_m_<>_width_G_&_m_<_k_)_)
percases ( m = width G or m <> width G ) ;
case m = width G ; ::_thesis: contradiction
then len f <= i by A3, A5, A30;
hence contradiction by A31, A33, XXREAL_0:1; ::_thesis: verum
end;
case m <> width G ; ::_thesis: m < k
then m < width G by A25, XXREAL_0:1;
then ( 1 <= m + 1 & m + 1 <= width G ) by NAT_1:11, NAT_1:13;
then A34: m + 1 in Seg (width G) by FINSEQ_1:1;
reconsider l = j - i as Element of NAT by A31, INT_1:5;
defpred S2[ set ] means for n, l being Element of NAT st n = $1 & n > 0 & i + n in dom f & f /. (i + n) in rng (Col (G,l)) & l in Seg (width G) holds
m < l;
A35: k in Seg (width G) by A26, FINSEQ_1:1;
m in Seg (width G) by A24, A25, FINSEQ_1:1;
then A36: f /. (i + 1) in rng (Col (G,(m + 1))) by A1, A3, A4, A27, A29, A30, A34, Th32;
A37: for o being Element of NAT st S2[o] holds
S2[o + 1]
proof
let o be Element of NAT ; ::_thesis: ( S2[o] implies S2[o + 1] )
assume A38: S2[o] ; ::_thesis: S2[o + 1]
let n, l be Element of NAT ; ::_thesis: ( n = o + 1 & n > 0 & i + n in dom f & f /. (i + n) in rng (Col (G,l)) & l in Seg (width G) implies m < l )
assume that
A39: n = o + 1 and
A40: n > 0 and
A41: i + n in dom f and
A42: f /. (i + n) in rng (Col (G,l)) and
A43: l in Seg (width G) ; ::_thesis: m < l
now__::_thesis:_m_<_l
percases ( o = 0 or o <> 0 ) ;
suppose o = 0 ; ::_thesis: m < l
then l = m + 1 by A34, A36, A39, A42, A43, Th4;
hence m < l by NAT_1:13; ::_thesis: verum
end;
supposeA44: o <> 0 ; ::_thesis: m < l
1 <= i by A27, FINSEQ_3:25;
then A45: 1 <= i + o by NAT_1:12;
( i + n <= len f & i + o <= (i + o) + 1 ) by A41, FINSEQ_3:25, NAT_1:12;
then i + o <= len f by A39, XXREAL_0:2;
then A46: i + o in dom f by A45, FINSEQ_3:25;
then consider l1 being Element of NAT such that
A47: l1 in Seg (width G) and
A48: f /. (i + o) in rng (Col (G,l1)) by A4, Th30;
A49: m < l1 by A38, A44, A46, A47, A48;
A50: i + n = (i + o) + 1 by A39;
now__::_thesis:_m_<_l
percases ( f /. (i + n) in rng (Col (G,l1)) or for k being Element of NAT st f /. (i + n) in rng (Col (G,k)) & k in Seg (width G) holds
abs (l1 - k) = 1 ) by A4, A41, A50, A46, A47, A48, Th31;
suppose f /. (i + n) in rng (Col (G,l1)) ; ::_thesis: m < l
hence m < l by A42, A43, A47, A49, Th4; ::_thesis: verum
end;
suppose for k being Element of NAT st f /. (i + n) in rng (Col (G,k)) & k in Seg (width G) holds
abs (l1 - k) = 1 ; ::_thesis: m < l
then A51: abs (l1 - l) = 1 by A42, A43;
now__::_thesis:_m_<_l
percases ( ( l1 > l & l1 = l + 1 ) or ( l1 < l & l = l1 + 1 ) ) by A51, SEQM_3:41;
suppose ( l1 > l & l1 = l + 1 ) ; ::_thesis: m < l
then A52: m <= l by A49, NAT_1:13;
now__::_thesis:_(_(_m_=_l_&_contradiction_)_or_(_m_<_l_&_m_<_l_)_)
percases ( m = l or m < l ) by A52, XXREAL_0:1;
case m = l ; ::_thesis: contradiction
then i + n <= i by A30, A41, A42;
then n <= i - i by XREAL_1:19;
hence contradiction by A40; ::_thesis: verum
end;
case m < l ; ::_thesis: m < l
hence m < l ; ::_thesis: verum
end;
end;
end;
hence m < l ; ::_thesis: verum
end;
suppose ( l1 < l & l = l1 + 1 ) ; ::_thesis: m < l
hence m < l by A49, XXREAL_0:2; ::_thesis: verum
end;
end;
end;
hence m < l ; ::_thesis: verum
end;
end;
end;
hence m < l ; ::_thesis: verum
end;
end;
end;
hence m < l ; ::_thesis: verum
end;
A53: S2[ 0 ] ;
A54: for o being Element of NAT holds S2[o] from NAT_1:sch_1(A53, A37);
( 0 < j - i & i + l = j ) by A31, XREAL_1:50;
hence m < k by A28, A32, A54, A35; ::_thesis: verum
end;
end;
end;
hence m < k ; ::_thesis: verum
end;
theorem Th34: :: GOBOARD1:34
for k, n being Element of NAT
for G being Go-board
for f being FinSequence of (TOP-REAL 2) st k in Seg (width G) & f /. 1 in rng (Col (G,1)) & f is_sequence_on G & ( for i being Element of NAT st i in dom f & f /. i in rng (Col (G,k)) holds
n <= i ) holds
for i being Element of NAT st i in dom f & i <= n holds
for m being Element of NAT st m in Seg (width G) & f /. i in rng (Col (G,m)) holds
m <= k
proof
let k, n be Element of NAT ; ::_thesis: for G being Go-board
for f being FinSequence of (TOP-REAL 2) st k in Seg (width G) & f /. 1 in rng (Col (G,1)) & f is_sequence_on G & ( for i being Element of NAT st i in dom f & f /. i in rng (Col (G,k)) holds
n <= i ) holds
for i being Element of NAT st i in dom f & i <= n holds
for m being Element of NAT st m in Seg (width G) & f /. i in rng (Col (G,m)) holds
m <= k
let G be Go-board; ::_thesis: for f being FinSequence of (TOP-REAL 2) st k in Seg (width G) & f /. 1 in rng (Col (G,1)) & f is_sequence_on G & ( for i being Element of NAT st i in dom f & f /. i in rng (Col (G,k)) holds
n <= i ) holds
for i being Element of NAT st i in dom f & i <= n holds
for m being Element of NAT st m in Seg (width G) & f /. i in rng (Col (G,m)) holds
m <= k
let f be FinSequence of (TOP-REAL 2); ::_thesis: ( k in Seg (width G) & f /. 1 in rng (Col (G,1)) & f is_sequence_on G & ( for i being Element of NAT st i in dom f & f /. i in rng (Col (G,k)) holds
n <= i ) implies for i being Element of NAT st i in dom f & i <= n holds
for m being Element of NAT st m in Seg (width G) & f /. i in rng (Col (G,m)) holds
m <= k )
assume that
A1: k in Seg (width G) and
A2: f /. 1 in rng (Col (G,1)) and
A3: f is_sequence_on G and
A4: for i being Element of NAT st i in dom f & f /. i in rng (Col (G,k)) holds
n <= i ; ::_thesis: for i being Element of NAT st i in dom f & i <= n holds
for m being Element of NAT st m in Seg (width G) & f /. i in rng (Col (G,m)) holds
m <= k
defpred S1[ Element of NAT ] means ( $1 in dom f & $1 <= n implies for m being Element of NAT st m in Seg (width G) & f /. $1 in rng (Col (G,m)) holds
m <= k );
A5: dom G = Seg (len G) by FINSEQ_1:def_3;
0 < width G by Lm1;
then 0 + 1 <= width G by NAT_1:13;
then A6: 1 in Seg (width G) by FINSEQ_1:1;
A7: 1 <= k by A1, FINSEQ_1:1;
A8: for i being Element of NAT st S1[i] holds
S1[i + 1]
proof
let i be Element of NAT ; ::_thesis: ( S1[i] implies S1[i + 1] )
assume A9: S1[i] ; ::_thesis: S1[i + 1]
assume that
A10: i + 1 in dom f and
A11: i + 1 <= n ; ::_thesis: for m being Element of NAT st m in Seg (width G) & f /. (i + 1) in rng (Col (G,m)) holds
m <= k
let m be Element of NAT ; ::_thesis: ( m in Seg (width G) & f /. (i + 1) in rng (Col (G,m)) implies m <= k )
assume A12: ( m in Seg (width G) & f /. (i + 1) in rng (Col (G,m)) ) ; ::_thesis: m <= k
now__::_thesis:_m_<=_k
percases ( i = 0 or i <> 0 ) ;
suppose i = 0 ; ::_thesis: m <= k
hence m <= k by A2, A6, A7, A12, Th4; ::_thesis: verum
end;
supposeA13: i <> 0 ; ::_thesis: m <= k
i + 1 <= len f by A10, FINSEQ_3:25;
then A14: i <= len f by NAT_1:13;
A15: i < n by A11, NAT_1:13;
A16: 0 + 1 <= i by A13, NAT_1:13;
then A17: i in dom f by A14, FINSEQ_3:25;
then consider i1, i2 being Element of NAT such that
A18: [i1,i2] in Indices G and
A19: f /. i = G * (i1,i2) by A3, Def9;
A20: Indices G = [:(dom G),(Seg (width G)):] by MATRIX_1:def_4;
then A21: i2 in Seg (width G) by A18, ZFMISC_1:87;
A22: ( dom (Col (G,i2)) = Seg (len (Col (G,i2))) & len (Col (G,i2)) = len G ) by FINSEQ_1:def_3, MATRIX_1:def_8;
A23: i1 in dom G by A18, A20, ZFMISC_1:87;
then (Col (G,i2)) . i1 = f /. i by A19, MATRIX_1:def_8;
then A24: f /. i in rng (Col (G,i2)) by A5, A23, A22, FUNCT_1:def_3;
then A25: i2 <= k by A9, A11, A16, A14, A21, FINSEQ_3:25, NAT_1:13;
now__::_thesis:_(_(_i2_<_k_&_m_<=_k_)_or_(_i2_=_k_&_contradiction_)_)
percases ( i2 < k or i2 = k ) by A25, XXREAL_0:1;
caseA26: i2 < k ; ::_thesis: m <= k
now__::_thesis:_m_<=_k
percases ( f /. (i + 1) in rng (Col (G,i2)) or for j being Element of NAT st f /. (i + 1) in rng (Col (G,j)) & j in Seg (width G) holds
abs (i2 - j) = 1 ) by A3, A10, A17, A21, A24, Th31;
suppose f /. (i + 1) in rng (Col (G,i2)) ; ::_thesis: m <= k
hence m <= k by A12, A21, A26, Th4; ::_thesis: verum
end;
suppose for j being Element of NAT st f /. (i + 1) in rng (Col (G,j)) & j in Seg (width G) holds
abs (i2 - j) = 1 ; ::_thesis: m <= k
then A27: abs (i2 - m) = 1 by A12;
now__::_thesis:_m_<=_k
percases ( ( i2 > m & i2 = m + 1 ) or ( i2 < m & m = i2 + 1 ) ) by A27, SEQM_3:41;
suppose ( i2 > m & i2 = m + 1 ) ; ::_thesis: m <= k
hence m <= k by A26, XXREAL_0:2; ::_thesis: verum
end;
suppose ( i2 < m & m = i2 + 1 ) ; ::_thesis: m <= k
hence m <= k by A26, NAT_1:13; ::_thesis: verum
end;
end;
end;
hence m <= k ; ::_thesis: verum
end;
end;
end;
hence m <= k ; ::_thesis: verum
end;
case i2 = k ; ::_thesis: contradiction
hence contradiction by A4, A15, A17, A24; ::_thesis: verum
end;
end;
end;
hence m <= k ; ::_thesis: verum
end;
end;
end;
hence m <= k ; ::_thesis: verum
end;
A28: S1[ 0 ] by FINSEQ_3:25;
thus for n being Element of NAT holds S1[n] from NAT_1:sch_1(A28, A8); ::_thesis: verum
end;
theorem :: GOBOARD1:35
for G being Go-board
for f being FinSequence of (TOP-REAL 2) st f is_sequence_on G & f /. 1 in rng (Col (G,1)) & f /. (len f) in rng (Col (G,(width G))) & width G > 1 & 1 <= len f holds
ex g being FinSequence of (TOP-REAL 2) st
( g /. 1 in rng (Col ((DelCol (G,(width G))),1)) & g /. (len g) in rng (Col ((DelCol (G,(width G))),(width (DelCol (G,(width G)))))) & 1 <= len g & g is_sequence_on DelCol (G,(width G)) & rng g c= rng f )
proof
let G be Go-board; ::_thesis: for f being FinSequence of (TOP-REAL 2) st f is_sequence_on G & f /. 1 in rng (Col (G,1)) & f /. (len f) in rng (Col (G,(width G))) & width G > 1 & 1 <= len f holds
ex g being FinSequence of (TOP-REAL 2) st
( g /. 1 in rng (Col ((DelCol (G,(width G))),1)) & g /. (len g) in rng (Col ((DelCol (G,(width G))),(width (DelCol (G,(width G)))))) & 1 <= len g & g is_sequence_on DelCol (G,(width G)) & rng g c= rng f )
let f be FinSequence of (TOP-REAL 2); ::_thesis: ( f is_sequence_on G & f /. 1 in rng (Col (G,1)) & f /. (len f) in rng (Col (G,(width G))) & width G > 1 & 1 <= len f implies ex g being FinSequence of (TOP-REAL 2) st
( g /. 1 in rng (Col ((DelCol (G,(width G))),1)) & g /. (len g) in rng (Col ((DelCol (G,(width G))),(width (DelCol (G,(width G)))))) & 1 <= len g & g is_sequence_on DelCol (G,(width G)) & rng g c= rng f ) )
set D = DelCol (G,(width G));
assume that
A1: f is_sequence_on G and
A2: f /. 1 in rng (Col (G,1)) and
A3: f /. (len f) in rng (Col (G,(width G))) and
A4: width G > 1 and
A5: 1 <= len f ; ::_thesis: ex g being FinSequence of (TOP-REAL 2) st
( g /. 1 in rng (Col ((DelCol (G,(width G))),1)) & g /. (len g) in rng (Col ((DelCol (G,(width G))),(width (DelCol (G,(width G)))))) & 1 <= len g & g is_sequence_on DelCol (G,(width G)) & rng g c= rng f )
consider k being Element of NAT such that
A6: width G = k + 1 and
A7: k > 0 by A4, SEQM_3:43;
A8: width G in Seg (width G) by A4, FINSEQ_1:1;
then A9: len (DelCol (G,(width G))) = len G by A4, Def8;
A10: 0 + 1 <= k by A7, NAT_1:13;
then 1 < width G by A6, NAT_1:13;
then A11: Col ((DelCol (G,(width G))),1) = Col (G,1) by A6, A7, A8, Th13;
A12: dom G = Seg (len G) by FINSEQ_1:def_3;
defpred S1[ Nat] means ( $1 in dom f & f /. $1 in rng (Col (G,k)) );
k <= k + 1 by NAT_1:11;
then ex m being Element of NAT st S1[m] by A1, A2, A3, A5, A6, A10, Th33;
then A13: ex m being Nat st S1[m] ;
consider m being Nat such that
A14: ( S1[m] & ( for i being Nat st S1[i] holds
m <= i ) ) from NAT_1:sch_5(A13);
A15: width (DelCol (G,(width G))) = k by A6, A7, A8, Th10;
then width (DelCol (G,(width G))) < width G by A6, NAT_1:13;
then A16: Col ((DelCol (G,(width G))),(width (DelCol (G,(width G))))) = Col (G,(width (DelCol (G,(width G))))) by A6, A10, A8, A15, Th13;
A17: dom (DelCol (G,(width G))) = Seg (len (DelCol (G,(width G)))) by FINSEQ_1:def_3;
A18: for i being Element of NAT st S1[i] holds
m <= i by A14;
reconsider m = m as Element of NAT by ORDINAL1:def_12;
A19: 1 <= m by A14, FINSEQ_3:25;
then A20: 1 in Seg m by FINSEQ_1:1;
A21: Indices G = [:(dom G),(Seg (width G)):] by MATRIX_1:def_4;
take t = f | m; ::_thesis: ( t /. 1 in rng (Col ((DelCol (G,(width G))),1)) & t /. (len t) in rng (Col ((DelCol (G,(width G))),(width (DelCol (G,(width G)))))) & 1 <= len t & t is_sequence_on DelCol (G,(width G)) & rng t c= rng f )
m <= len f by A14, FINSEQ_3:25;
then A22: len t = m by FINSEQ_1:59;
then len t in Seg m by A19, FINSEQ_1:1;
hence ( t /. 1 in rng (Col ((DelCol (G,(width G))),1)) & t /. (len t) in rng (Col ((DelCol (G,(width G))),(width (DelCol (G,(width G)))))) & 1 <= len t ) by A2, A14, A15, A11, A16, A22, A20, FINSEQ_1:1, FINSEQ_4:71; ::_thesis: ( t is_sequence_on DelCol (G,(width G)) & rng t c= rng f )
A23: dom t = Seg (len t) by FINSEQ_1:def_3;
A24: Indices (DelCol (G,(width G))) = [:(dom (DelCol (G,(width G)))),(Seg (width (DelCol (G,(width G))))):] by MATRIX_1:def_4;
A25: now__::_thesis:_for_n_being_Element_of_NAT_st_n_in_dom_t_holds_
ex_i,_j_being_Element_of_NAT_st_
(_[i,j]_in_Indices_(DelCol_(G,(width_G)))_&_t_/._n_=_(DelCol_(G,(width_G)))_*_(i,j)_)
k <= k + 1 by NAT_1:11;
then A26: k in Seg (width G) by A6, A10, FINSEQ_1:1;
let n be Element of NAT ; ::_thesis: ( n in dom t implies ex i, j being Element of NAT st
( [i,j] in Indices (DelCol (G,(width G))) & t /. n = (DelCol (G,(width G))) * (i,j) ) )
assume A27: n in dom t ; ::_thesis: ex i, j being Element of NAT st
( [i,j] in Indices (DelCol (G,(width G))) & t /. n = (DelCol (G,(width G))) * (i,j) )
then A28: n <= m by A22, FINSEQ_3:25;
A29: n in dom f by A14, A22, A23, A27, FINSEQ_4:71;
then consider i, j being Element of NAT such that
A30: [i,j] in Indices G and
A31: f /. n = G * (i,j) by A1, Def9;
A32: j in Seg (width G) by A21, A30, ZFMISC_1:87;
then A33: 1 <= j by FINSEQ_1:1;
take i = i; ::_thesis: ex j being Element of NAT st
( [i,j] in Indices (DelCol (G,(width G))) & t /. n = (DelCol (G,(width G))) * (i,j) )
take j = j; ::_thesis: ( [i,j] in Indices (DelCol (G,(width G))) & t /. n = (DelCol (G,(width G))) * (i,j) )
A34: ( len (Col (G,j)) = len G & dom (Col (G,j)) = Seg (len (Col (G,j))) ) by FINSEQ_1:def_3, MATRIX_1:def_8;
A35: i in dom G by A21, A30, ZFMISC_1:87;
then (Col (G,j)) . i = G * (i,j) by MATRIX_1:def_8;
then f /. n in rng (Col (G,j)) by A12, A31, A35, A34, FUNCT_1:def_3;
then j <= k by A1, A2, A18, A29, A28, A32, A26, Th34;
then A36: j in Seg k by A33, FINSEQ_1:1;
hence [i,j] in Indices (DelCol (G,(width G))) by A9, A12, A17, A15, A24, A35, ZFMISC_1:87; ::_thesis: t /. n = (DelCol (G,(width G))) * (i,j)
thus t /. n = G * (i,j) by A14, A22, A23, A27, A31, FINSEQ_4:71
.= (DelCol (G,(width G))) * (i,j) by A6, A7, A35, A36, Th20 ; ::_thesis: verum
end;
now__::_thesis:_for_n_being_Element_of_NAT_st_n_in_dom_t_&_n_+_1_in_dom_t_holds_
for_i1,_i2,_j1,_j2_being_Element_of_NAT_st_[i1,i2]_in_Indices_(DelCol_(G,(width_G)))_&_[j1,j2]_in_Indices_(DelCol_(G,(width_G)))_&_t_/._n_=_(DelCol_(G,(width_G)))_*_(i1,i2)_&_t_/._(n_+_1)_=_(DelCol_(G,(width_G)))_*_(j1,j2)_holds_
(abs_(i1_-_j1))_+_(abs_(i2_-_j2))_=_1
let n be Element of NAT ; ::_thesis: ( n in dom t & n + 1 in dom t implies for i1, i2, j1, j2 being Element of NAT st [i1,i2] in Indices (DelCol (G,(width G))) & [j1,j2] in Indices (DelCol (G,(width G))) & t /. n = (DelCol (G,(width G))) * (i1,i2) & t /. (n + 1) = (DelCol (G,(width G))) * (j1,j2) holds
(abs (i1 - j1)) + (abs (i2 - j2)) = 1 )
assume that
A37: n in dom t and
A38: n + 1 in dom t ; ::_thesis: for i1, i2, j1, j2 being Element of NAT st [i1,i2] in Indices (DelCol (G,(width G))) & [j1,j2] in Indices (DelCol (G,(width G))) & t /. n = (DelCol (G,(width G))) * (i1,i2) & t /. (n + 1) = (DelCol (G,(width G))) * (j1,j2) holds
(abs (i1 - j1)) + (abs (i2 - j2)) = 1
A39: ( n in dom f & n + 1 in dom f ) by A14, A22, A23, A37, A38, FINSEQ_4:71;
let i1, i2, j1, j2 be Element of NAT ; ::_thesis: ( [i1,i2] in Indices (DelCol (G,(width G))) & [j1,j2] in Indices (DelCol (G,(width G))) & t /. n = (DelCol (G,(width G))) * (i1,i2) & t /. (n + 1) = (DelCol (G,(width G))) * (j1,j2) implies (abs (i1 - j1)) + (abs (i2 - j2)) = 1 )
assume that
A40: [i1,i2] in Indices (DelCol (G,(width G))) and
A41: [j1,j2] in Indices (DelCol (G,(width G))) and
A42: t /. n = (DelCol (G,(width G))) * (i1,i2) and
A43: t /. (n + 1) = (DelCol (G,(width G))) * (j1,j2) ; ::_thesis: (abs (i1 - j1)) + (abs (i2 - j2)) = 1
A44: ( i1 in dom (DelCol (G,(width G))) & i2 in Seg k ) by A15, A24, A40, ZFMISC_1:87;
A45: ( j1 in dom (DelCol (G,(width G))) & j2 in Seg k ) by A15, A24, A41, ZFMISC_1:87;
t /. n = f /. n by A14, A22, A23, A37, FINSEQ_4:71;
then A46: f /. n = G * (i1,i2) by A6, A7, A9, A12, A17, A42, A44, Th20;
k <= k + 1 by NAT_1:11;
then A47: Seg k c= Seg (width G) by A6, FINSEQ_1:5;
then A48: [j1,j2] in Indices G by A9, A21, A12, A17, A45, ZFMISC_1:87;
t /. (n + 1) = f /. (n + 1) by A14, A22, A23, A38, FINSEQ_4:71;
then A49: f /. (n + 1) = G * (j1,j2) by A6, A7, A9, A12, A17, A43, A45, Th20;
[i1,i2] in Indices G by A9, A21, A12, A17, A44, A47, ZFMISC_1:87;
hence (abs (i1 - j1)) + (abs (i2 - j2)) = 1 by A1, A39, A46, A49, A48, Def9; ::_thesis: verum
end;
hence t is_sequence_on DelCol (G,(width G)) by A25, Def9; ::_thesis: rng t c= rng f
t = f | (Seg m) by FINSEQ_1:def_15;
hence rng t c= rng f by RELAT_1:70; ::_thesis: verum
end;
theorem :: GOBOARD1:36
for G being Go-board
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 )
proof
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;
percases ( n = m or n > m or n < m ) by XXREAL_0:1;
supposeA12: 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 )
reconsider h = <*x*> as FinSequence of (TOP-REAL 2) ;
A13: len h = 1 by FINSEQ_1:39;
A14: now__::_thesis:_for_k_being_Element_of_NAT_st_k_in_Seg_1_holds_
h_/._k_=_x
let k be Element of 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;
A17: rng h c= rng f
proof
let z be set ; :: 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;
reconsider h = h as FinSequence of (TOP-REAL 2) ;
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_Element_of_NAT_st_i_in_dom_h_&_i_+_1_in_dom_h_holds_
for_i1,_i2,_j1,_j2_being_Element_of_NAT_st_[i1,i2]_in_Indices_G_&_[j1,j2]_in_Indices_G_&_h_/._i_=_G_*_(i1,i2)_&_h_/._(i_+_1)_=_G_*_(j1,j2)_holds_
(abs_(i1_-_j1))_+_(abs_(i2_-_j2))_=_1
let i be Element of NAT ; ::_thesis: ( i in dom h & i + 1 in dom h implies for i1, i2, j1, j2 being Element of NAT st [i1,i2] in Indices G & [j1,j2] in Indices G & h /. i = G * (i1,i2) & h /. (i + 1) = G * (j1,j2) holds
(abs (i1 - j1)) + (abs (i2 - j2)) = 1 )
assume that
A22: i in dom h and
A23: i + 1 in dom h ; ::_thesis: for i1, i2, j1, j2 being Element of NAT st [i1,i2] in Indices G & [j1,j2] in Indices G & h /. i = G * (i1,i2) & h /. (i + 1) = G * (j1,j2) holds
(abs (i1 - j1)) + (abs (i2 - j2)) = 1
i = 1 by A13, A20, A22, FINSEQ_1:2, TARSKI:def_1;
hence for i1, i2, j1, j2 being Element of NAT st [i1,i2] in Indices G & [j1,j2] in Indices G & h /. i = G * (i1,i2) & h /. (i + 1) = G * (j1,j2) holds
(abs (i1 - j1)) + (abs (i2 - j2)) = 1 by A13, A20, A23, FINSEQ_1:2, TARSKI:def_1; ::_thesis: verum
end;
now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_dom_h_holds_
ex_i1,_i2_being_Element_of_NAT_st_
(_[i1,i2]_in_Indices_G_&_h_/._i_=_G_*_(i1,i2)_)
consider i1, i2 being Element of NAT such that
A24: ( [i1,i2] in Indices G & f /. n = G * (i1,i2) ) by A1, A9, Def9;
let i be Element of NAT ; ::_thesis: ( i in dom h implies ex i1, i2 being Element of NAT st
( [i1,i2] in Indices G & h /. i = G * (i1,i2) ) )
assume A25: i in dom h ; ::_thesis: ex i1, i2 being Element of NAT st
( [i1,i2] in Indices G & h /. i = G * (i1,i2) )
take i1 = i1; ::_thesis: ex i2 being Element of 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;
hence ( 1 <= len h & h is_sequence_on G ) by A21, Def9, FINSEQ_1:39; ::_thesis: verum
end;
supposeA26: 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 )
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 S1[ Nat, set ] means for k being Element of NAT st $1 + k = n + 1 holds
$2 = (f | n) /. k;
A27: n in Seg n by A11, FINSEQ_1:1;
A28: now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_Seg_l_holds_
(n_+_1)_-_i_is_Element_of_NAT
let i be Element of 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;
A30: for i being Nat st i in Seg l holds
ex p being Point of (TOP-REAL 2) st S1[i,p]
proof
let i be Nat; ::_thesis: ( i in Seg l implies ex p being Point of (TOP-REAL 2) st S1[i,p] )
assume i in Seg l ; ::_thesis: ex p being Point of (TOP-REAL 2) st S1[i,p]
then reconsider a = (n + 1) - i as Element of NAT by A28;
take (f | n) /. a ; ::_thesis: S1[i,(f | n) /. a]
let k be Element of 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;
consider g being FinSequence of (TOP-REAL 2) such that
A31: ( len g = l & ( for i being Nat st i in Seg l holds
S1[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 Element of 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
let i be Element of 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;
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
let z be set ; :: 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;
A40: dom g = Seg (len g) by FINSEQ_1:def_3;
A41: now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_dom_g_&_i_+_1_in_dom_g_holds_
for_i1,_i2,_j1,_j2_being_Element_of_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_=_(abs_(i1_-_j1))_+_(abs_(i2_-_j2))
let i be Element of NAT ; ::_thesis: ( i in dom g & i + 1 in dom g implies for i1, i2, j1, j2 being Element of 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 = (abs (i1 - j1)) + (abs (i2 - j2)) )
assume that
A42: i in dom g and
A43: i + 1 in dom g ; ::_thesis: for i1, i2, j1, j2 being Element of 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 = (abs (i1 - j1)) + (abs (i2 - j2))
let i1, i2, j1, j2 be Element of 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 = (abs (i1 - j1)) + (abs (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 = (abs (i1 - j1)) + (abs (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 = (abs (j1 - i1)) + (abs (j2 - i2)) by A1, A47, A45, A46, A44, Def9
.= (abs (- (i1 - j1))) + (abs (- (i2 - j2)))
.= (abs (i1 - j1)) + (abs (- (i2 - j2))) by COMPLEX1:52
.= (abs (i1 - j1)) + (abs (i2 - j2)) by COMPLEX1:52 ;
::_thesis: verum
end;
m + 1 <= n by A26, NAT_1:13;
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_Element_of_NAT_st_i_in_dom_g_holds_
ex_i1,_i2_being_Element_of_NAT_st_
(_[i1,i2]_in_Indices_G_&_g_/._i_=_G_*_(i1,i2)_)
let i be Element of NAT ; ::_thesis: ( i in dom g implies ex i1, i2 being Element of NAT st
( [i1,i2] in Indices G & g /. i = G * (i1,i2) ) )
assume A52: i in dom g ; ::_thesis: ex i1, i2 being Element of 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 Element of NAT such that
A53: ( [i1,i2] in Indices G & f /. ww = G * (i1,i2) ) by A1, Def9;
take i1 = i1; ::_thesis: ex i2 being Element of 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;
hence ( 1 <= len g & g is_sequence_on G ) by A31, A48, A41, Def9, XREAL_1:19; ::_thesis: verum
end;
supposeA54: 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 )
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 S1[ 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 S1[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
S1[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 Element of 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 Element of 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;
A63: now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_dom_g_&_i_+_1_in_dom_g_holds_
for_i1,_i2,_j1,_j2_being_Element_of_NAT_st_[i1,i2]_in_Indices_G_&_[j1,j2]_in_Indices_G_&_g_/._i_=_G_*_(i1,i2)_&_g_/._(i_+_1)_=_G_*_(j1,j2)_holds_
(abs_(i1_-_j1))_+_(abs_(i2_-_j2))_=_1
let i be Element of NAT ; ::_thesis: ( i in dom g & i + 1 in dom g implies for i1, i2, j1, j2 being Element of NAT st [i1,i2] in Indices G & [j1,j2] in Indices G & g /. i = G * (i1,i2) & g /. (i + 1) = G * (j1,j2) holds
(abs (i1 - j1)) + (abs (i2 - j2)) = 1 )
assume that
A64: i in dom g and
A65: i + 1 in dom g ; ::_thesis: for i1, i2, j1, j2 being Element of NAT st [i1,i2] in Indices G & [j1,j2] in Indices G & g /. i = G * (i1,i2) & g /. (i + 1) = G * (j1,j2) holds
(abs (i1 - j1)) + (abs (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 Element of NAT ; ::_thesis: ( [i1,i2] in Indices G & [j1,j2] in Indices G & g /. i = G * (i1,i2) & g /. (i + 1) = G * (j1,j2) implies (abs (i1 - j1)) + (abs (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: (abs (i1 - j1)) + (abs (i2 - j2)) = 1
w + i in dom f by A60, A59, A64;
hence (abs (i1 - j1)) + (abs (i2 - j2)) = 1 by A1, A66, A67, A68, Def9; ::_thesis: verum
end;
A69: dom g = Seg (len g) by FINSEQ_1:def_3;
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
let z be set ; :: 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;
n + 1 <= m by A54, NAT_1:13;
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_Element_of_NAT_st_i_in_dom_g_holds_
ex_i1,_i2_being_Element_of_NAT_st_
(_[i1,i2]_in_Indices_G_&_g_/._i_=_G_*_(i1,i2)_)
let i be Element of NAT ; ::_thesis: ( i in dom g implies ex i1, i2 being Element of NAT st
( [i1,i2] in Indices G & g /. i = G * (i1,i2) ) )
assume A75: i in dom g ; ::_thesis: ex i1, i2 being Element of 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 Element of NAT such that
A76: ( [i1,i2] in Indices G & f /. (w + i) = G * (i1,i2) ) by A1, Def9;
take i1 = i1; ::_thesis: ex i2 being Element of 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;
hence ( 1 <= len g & g is_sequence_on G ) by A57, A73, A63, Def9, XREAL_1:19; ::_thesis: verum
end;
end;
end;
theorem :: GOBOARD1:37
for k, n being Element of NAT
for G being Go-board
for f being FinSequence of (TOP-REAL 2) st k in dom G & f is_sequence_on G & f /. (len f) in rng (Line (G,(len G))) & n in dom f & f /. n in rng (Line (G,k)) holds
( ( for i being Element of NAT st k <= i & i <= len G holds
ex j being Element of NAT st
( j in dom f & n <= j & f /. j in rng (Line (G,i)) ) ) & ( for i being Element of NAT st k < i & i <= len G holds
ex j being Element of NAT st
( j in dom f & n < j & f /. j in rng (Line (G,i)) ) ) )
proof
let k, n be Element of NAT ; ::_thesis: for G being Go-board
for f being FinSequence of (TOP-REAL 2) st k in dom G & f is_sequence_on G & f /. (len f) in rng (Line (G,(len G))) & n in dom f & f /. n in rng (Line (G,k)) holds
( ( for i being Element of NAT st k <= i & i <= len G holds
ex j being Element of NAT st
( j in dom f & n <= j & f /. j in rng (Line (G,i)) ) ) & ( for i being Element of NAT st k < i & i <= len G holds
ex j being Element of NAT st
( j in dom f & n < j & f /. j in rng (Line (G,i)) ) ) )
let G be Go-board; ::_thesis: for f being FinSequence of (TOP-REAL 2) st k in dom G & f is_sequence_on G & f /. (len f) in rng (Line (G,(len G))) & n in dom f & f /. n in rng (Line (G,k)) holds
( ( for i being Element of NAT st k <= i & i <= len G holds
ex j being Element of NAT st
( j in dom f & n <= j & f /. j in rng (Line (G,i)) ) ) & ( for i being Element of NAT st k < i & i <= len G holds
ex j being Element of NAT st
( j in dom f & n < j & f /. j in rng (Line (G,i)) ) ) )
let f be FinSequence of (TOP-REAL 2); ::_thesis: ( k in dom G & f is_sequence_on G & f /. (len f) in rng (Line (G,(len G))) & n in dom f & f /. n in rng (Line (G,k)) implies ( ( for i being Element of NAT st k <= i & i <= len G holds
ex j being Element of NAT st
( j in dom f & n <= j & f /. j in rng (Line (G,i)) ) ) & ( for i being Element of NAT st k < i & i <= len G holds
ex j being Element of NAT st
( j in dom f & n < j & f /. j in rng (Line (G,i)) ) ) ) )
assume that
A1: k in dom G and
A2: ( f is_sequence_on G & f /. (len f) in rng (Line (G,(len G))) ) and
A3: n in dom f and
A4: f /. n in rng (Line (G,k)) ; ::_thesis: ( ( for i being Element of NAT st k <= i & i <= len G holds
ex j being Element of NAT st
( j in dom f & n <= j & f /. j in rng (Line (G,i)) ) ) & ( for i being Element of NAT st k < i & i <= len G holds
ex j being Element of NAT st
( j in dom f & n < j & f /. j in rng (Line (G,i)) ) ) )
defpred S1[ Element of NAT ] means ( k <= $1 & $1 <= len G implies ex j being Element of NAT st
( j in dom f & n <= j & f /. j in rng (Line (G,$1)) ) );
A5: 1 <= k by A1, FINSEQ_3:25;
A6: ( 1 <= n & n <= len f ) by A3, FINSEQ_3:25;
A7: for i being Element of NAT st S1[i] holds
S1[i + 1]
proof
let i be Element of NAT ; ::_thesis: ( S1[i] implies S1[i + 1] )
assume A8: S1[i] ; ::_thesis: S1[i + 1]
assume that
A9: k <= i + 1 and
A10: i + 1 <= len G ; ::_thesis: ex j being Element of NAT st
( j in dom f & n <= j & f /. j in rng (Line (G,(i + 1))) )
now__::_thesis:_ex_j_being_Element_of_NAT_st_
(_j_in_dom_f_&_n_<=_j_&_f_/._j_in_rng_(Line_(G,(i_+_1)))_)
percases ( k = i + 1 or k < i + 1 ) by A9, XXREAL_0:1;
supposeA11: k = i + 1 ; ::_thesis: ex j being Element of NAT st
( j in dom f & n <= j & f /. j in rng (Line (G,(i + 1))) )
take j = n; ::_thesis: ( j in dom f & n <= j & f /. j in rng (Line (G,(i + 1))) )
thus ( j in dom f & n <= j & f /. j in rng (Line (G,(i + 1))) ) by A3, A4, A11; ::_thesis: verum
end;
supposeA12: k < i + 1 ; ::_thesis: ex j being Element of NAT st
( j in dom f & n <= j & f /. j in rng (Line (G,(i + 1))) )
then k <= i by NAT_1:13;
then A13: 1 <= i by A5, XXREAL_0:2;
i <= len G by A10, NAT_1:13;
then A14: i in dom G by A13, FINSEQ_3:25;
1 <= i + 1 by A5, A12, XXREAL_0:2;
then A15: i + 1 in dom G by A10, FINSEQ_3:25;
defpred S2[ Nat] means ( $1 in dom f & n <= $1 & f /. $1 in rng (Line (G,i)) );
A16: for j being Nat st S2[j] holds
j <= len f by FINSEQ_3:25;
A17: ex j being Nat st S2[j] by A8, A10, A12, NAT_1:13;
consider ma being Nat such that
A18: ( S2[ma] & ( for j being Nat st S2[j] holds
j <= ma ) ) from NAT_1:sch_6(A16, A17);
A19: now__::_thesis:_for_j_being_Element_of_NAT_st_j_in_dom_f_&_f_/._j_in_rng_(Line_(G,i))_holds_
j_<=_ma
let j be Element of NAT ; ::_thesis: ( j in dom f & f /. j in rng (Line (G,i)) implies j <= ma )
assume A20: ( j in dom f & f /. j in rng (Line (G,i)) ) ; ::_thesis: j <= ma
now__::_thesis:_j_<=_ma
percases ( j < n or n <= j ) ;
suppose j < n ; ::_thesis: j <= ma
hence j <= ma by A18, XXREAL_0:2; ::_thesis: verum
end;
suppose n <= j ; ::_thesis: j <= ma
hence j <= ma by A18, A20; ::_thesis: verum
end;
end;
end;
hence j <= ma ; ::_thesis: verum
end;
take j = ma + 1; ::_thesis: ( j in dom f & n <= j & f /. j in rng (Line (G,(i + 1))) )
A21: 1 <= len f by A6, XXREAL_0:2;
hence j in dom f by A2, A14, A15, A18, A19, Th28; ::_thesis: ( n <= j & f /. j in rng (Line (G,(i + 1))) )
ma <= ma + 1 by NAT_1:11;
hence ( n <= j & f /. j in rng (Line (G,(i + 1))) ) by A2, A14, A15, A18, A21, A19, Th28, XXREAL_0:2; ::_thesis: verum
end;
end;
end;
hence ex j being Element of NAT st
( j in dom f & n <= j & f /. j in rng (Line (G,(i + 1))) ) ; ::_thesis: verum
end;
A22: S1[ 0 ] by A1, FINSEQ_3:25;
thus A23: for i being Element of NAT holds S1[i] from NAT_1:sch_1(A22, A7); ::_thesis: for i being Element of NAT st k < i & i <= len G holds
ex j being Element of NAT st
( j in dom f & n < j & f /. j in rng (Line (G,i)) )
let i be Element of NAT ; ::_thesis: ( k < i & i <= len G implies ex j being Element of NAT st
( j in dom f & n < j & f /. j in rng (Line (G,i)) ) )
assume that
A24: k < i and
A25: i <= len G ; ::_thesis: ex j being Element of NAT st
( j in dom f & n < j & f /. j in rng (Line (G,i)) )
consider j being Element of NAT such that
A26: j in dom f and
A27: n <= j and
A28: f /. j in rng (Line (G,i)) by A23, A24, A25;
take j ; ::_thesis: ( j in dom f & n < j & f /. j in rng (Line (G,i)) )
thus j in dom f by A26; ::_thesis: ( n < j & f /. j in rng (Line (G,i)) )
1 <= i by A5, A24, XXREAL_0:2;
then i in dom G by A25, FINSEQ_3:25;
then n <> j by A1, A4, A24, A28, Th3;
hence ( n < j & f /. j in rng (Line (G,i)) ) by A27, A28, XXREAL_0:1; ::_thesis: verum
end;