:: 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;