:: GOBOARD5 semantic presentation begin definition let G be Matrix of (TOP-REAL 2); let i be Nat; func v_strip (G,i) -> Subset of (TOP-REAL 2) equals :Def1: :: GOBOARD5:def 1 { |[r,s]| where r, s is Real : ( (G * (i,1)) `1 <= r & r <= (G * ((i + 1),1)) `1 ) } if ( 1 <= i & i < len G ) { |[r,s]| where r, s is Real : (G * (i,1)) `1 <= r } if i >= len G otherwise { |[r,s]| where r, s is Real : r <= (G * ((i + 1),1)) `1 } ; coherence ( ( 1 <= i & i < len G implies { |[r,s]| where r, s is Real : ( (G * (i,1)) `1 <= r & r <= (G * ((i + 1),1)) `1 ) } is Subset of (TOP-REAL 2) ) & ( i >= len G implies { |[r,s]| where r, s is Real : (G * (i,1)) `1 <= r } is Subset of (TOP-REAL 2) ) & ( ( not 1 <= i or not i < len G ) & not i >= len G implies { |[r,s]| where r, s is Real : r <= (G * ((i + 1),1)) `1 } is Subset of (TOP-REAL 2) ) ) proof hereby ::_thesis: ( ( i >= len G implies { |[r,s]| where r, s is Real : (G * (i,1)) `1 <= r } is Subset of (TOP-REAL 2) ) & ( ( not 1 <= i or not i < len G ) & not i >= len G implies { |[r,s]| where r, s is Real : r <= (G * ((i + 1),1)) `1 } is Subset of (TOP-REAL 2) ) ) assume that 1 <= i and i < len G ; ::_thesis: { |[r,s]| where r, s is Real : ( (G * (i,1)) `1 <= r & r <= (G * ((i + 1),1)) `1 ) } is Subset of (TOP-REAL 2) set A = { |[r,s]| where r, s is Real : ( (G * (i,1)) `1 <= r & r <= (G * ((i + 1),1)) `1 ) } ; { |[r,s]| where r, s is Real : ( (G * (i,1)) `1 <= r & r <= (G * ((i + 1),1)) `1 ) } c= the carrier of (TOP-REAL 2) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { |[r,s]| where r, s is Real : ( (G * (i,1)) `1 <= r & r <= (G * ((i + 1),1)) `1 ) } or x in the carrier of (TOP-REAL 2) ) assume x in { |[r,s]| where r, s is Real : ( (G * (i,1)) `1 <= r & r <= (G * ((i + 1),1)) `1 ) } ; ::_thesis: x in the carrier of (TOP-REAL 2) then ex r, s being Real st ( x = |[r,s]| & (G * (i,1)) `1 <= r & r <= (G * ((i + 1),1)) `1 ) ; hence x in the carrier of (TOP-REAL 2) ; ::_thesis: verum end; hence { |[r,s]| where r, s is Real : ( (G * (i,1)) `1 <= r & r <= (G * ((i + 1),1)) `1 ) } is Subset of (TOP-REAL 2) ; ::_thesis: verum end; hereby ::_thesis: ( ( not 1 <= i or not i < len G ) & not i >= len G implies { |[r,s]| where r, s is Real : r <= (G * ((i + 1),1)) `1 } is Subset of (TOP-REAL 2) ) assume i >= len G ; ::_thesis: { |[r,s]| where r, s is Real : (G * (i,1)) `1 <= r } is Subset of (TOP-REAL 2) set A = { |[r,s]| where r, s is Real : (G * (i,1)) `1 <= r } ; { |[r,s]| where r, s is Real : (G * (i,1)) `1 <= r } c= the carrier of (TOP-REAL 2) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { |[r,s]| where r, s is Real : (G * (i,1)) `1 <= r } or x in the carrier of (TOP-REAL 2) ) assume x in { |[r,s]| where r, s is Real : (G * (i,1)) `1 <= r } ; ::_thesis: x in the carrier of (TOP-REAL 2) then ex r, s being Real st ( x = |[r,s]| & (G * (i,1)) `1 <= r ) ; hence x in the carrier of (TOP-REAL 2) ; ::_thesis: verum end; hence { |[r,s]| where r, s is Real : (G * (i,1)) `1 <= r } is Subset of (TOP-REAL 2) ; ::_thesis: verum end; assume that ( not 1 <= i or not i < len G ) and i < len G ; ::_thesis: { |[r,s]| where r, s is Real : r <= (G * ((i + 1),1)) `1 } is Subset of (TOP-REAL 2) set A = { |[r,s]| where r, s is Real : r <= (G * ((i + 1),1)) `1 } ; { |[r,s]| where r, s is Real : r <= (G * ((i + 1),1)) `1 } c= the carrier of (TOP-REAL 2) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { |[r,s]| where r, s is Real : r <= (G * ((i + 1),1)) `1 } or x in the carrier of (TOP-REAL 2) ) assume x in { |[r,s]| where r, s is Real : r <= (G * ((i + 1),1)) `1 } ; ::_thesis: x in the carrier of (TOP-REAL 2) then ex r, s being Real st ( x = |[r,s]| & r <= (G * ((i + 1),1)) `1 ) ; hence x in the carrier of (TOP-REAL 2) ; ::_thesis: verum end; hence { |[r,s]| where r, s is Real : r <= (G * ((i + 1),1)) `1 } is Subset of (TOP-REAL 2) ; ::_thesis: verum end; correctness consistency for b1 being Subset of (TOP-REAL 2) st 1 <= i & i < len G & i >= len G holds ( b1 = { |[r,s]| where r, s is Real : ( (G * (i,1)) `1 <= r & r <= (G * ((i + 1),1)) `1 ) } iff b1 = { |[r,s]| where r, s is Real : (G * (i,1)) `1 <= r } ); ; func h_strip (G,i) -> Subset of (TOP-REAL 2) equals :Def2: :: GOBOARD5:def 2 { |[r,s]| where r, s is Real : ( (G * (1,i)) `2 <= s & s <= (G * (1,(i + 1))) `2 ) } if ( 1 <= i & i < width G ) { |[r,s]| where r, s is Real : (G * (1,i)) `2 <= s } if i >= width G otherwise { |[r,s]| where r, s is Real : s <= (G * (1,(i + 1))) `2 } ; coherence ( ( 1 <= i & i < width G implies { |[r,s]| where r, s is Real : ( (G * (1,i)) `2 <= s & s <= (G * (1,(i + 1))) `2 ) } is Subset of (TOP-REAL 2) ) & ( i >= width G implies { |[r,s]| where r, s is Real : (G * (1,i)) `2 <= s } is Subset of (TOP-REAL 2) ) & ( ( not 1 <= i or not i < width G ) & not i >= width G implies { |[r,s]| where r, s is Real : s <= (G * (1,(i + 1))) `2 } is Subset of (TOP-REAL 2) ) ) proof hereby ::_thesis: ( ( i >= width G implies { |[r,s]| where r, s is Real : (G * (1,i)) `2 <= s } is Subset of (TOP-REAL 2) ) & ( ( not 1 <= i or not i < width G ) & not i >= width G implies { |[r,s]| where r, s is Real : s <= (G * (1,(i + 1))) `2 } is Subset of (TOP-REAL 2) ) ) assume that 1 <= i and i < width G ; ::_thesis: { |[r,s]| where r, s is Real : ( (G * (1,i)) `2 <= s & s <= (G * (1,(i + 1))) `2 ) } is Subset of (TOP-REAL 2) set A = { |[r,s]| where r, s is Real : ( (G * (1,i)) `2 <= s & s <= (G * (1,(i + 1))) `2 ) } ; { |[r,s]| where r, s is Real : ( (G * (1,i)) `2 <= s & s <= (G * (1,(i + 1))) `2 ) } c= the carrier of (TOP-REAL 2) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { |[r,s]| where r, s is Real : ( (G * (1,i)) `2 <= s & s <= (G * (1,(i + 1))) `2 ) } or x in the carrier of (TOP-REAL 2) ) assume x in { |[r,s]| where r, s is Real : ( (G * (1,i)) `2 <= s & s <= (G * (1,(i + 1))) `2 ) } ; ::_thesis: x in the carrier of (TOP-REAL 2) then ex r, s being Real st ( x = |[r,s]| & (G * (1,i)) `2 <= s & s <= (G * (1,(i + 1))) `2 ) ; hence x in the carrier of (TOP-REAL 2) ; ::_thesis: verum end; hence { |[r,s]| where r, s is Real : ( (G * (1,i)) `2 <= s & s <= (G * (1,(i + 1))) `2 ) } is Subset of (TOP-REAL 2) ; ::_thesis: verum end; hereby ::_thesis: ( ( not 1 <= i or not i < width G ) & not i >= width G implies { |[r,s]| where r, s is Real : s <= (G * (1,(i + 1))) `2 } is Subset of (TOP-REAL 2) ) assume i >= width G ; ::_thesis: { |[r,s]| where r, s is Real : (G * (1,i)) `2 <= s } is Subset of (TOP-REAL 2) set A = { |[r,s]| where r, s is Real : (G * (1,i)) `2 <= s } ; { |[r,s]| where r, s is Real : (G * (1,i)) `2 <= s } c= the carrier of (TOP-REAL 2) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { |[r,s]| where r, s is Real : (G * (1,i)) `2 <= s } or x in the carrier of (TOP-REAL 2) ) assume x in { |[r,s]| where r, s is Real : (G * (1,i)) `2 <= s } ; ::_thesis: x in the carrier of (TOP-REAL 2) then ex r, s being Real st ( x = |[r,s]| & (G * (1,i)) `2 <= s ) ; hence x in the carrier of (TOP-REAL 2) ; ::_thesis: verum end; hence { |[r,s]| where r, s is Real : (G * (1,i)) `2 <= s } is Subset of (TOP-REAL 2) ; ::_thesis: verum end; assume that ( not 1 <= i or not i < width G ) and i < width G ; ::_thesis: { |[r,s]| where r, s is Real : s <= (G * (1,(i + 1))) `2 } is Subset of (TOP-REAL 2) set A = { |[r,s]| where r, s is Real : s <= (G * (1,(i + 1))) `2 } ; { |[r,s]| where r, s is Real : s <= (G * (1,(i + 1))) `2 } c= the carrier of (TOP-REAL 2) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { |[r,s]| where r, s is Real : s <= (G * (1,(i + 1))) `2 } or x in the carrier of (TOP-REAL 2) ) assume x in { |[r,s]| where r, s is Real : s <= (G * (1,(i + 1))) `2 } ; ::_thesis: x in the carrier of (TOP-REAL 2) then ex r, s being Real st ( x = |[r,s]| & s <= (G * (1,(i + 1))) `2 ) ; hence x in the carrier of (TOP-REAL 2) ; ::_thesis: verum end; hence { |[r,s]| where r, s is Real : s <= (G * (1,(i + 1))) `2 } is Subset of (TOP-REAL 2) ; ::_thesis: verum end; correctness consistency for b1 being Subset of (TOP-REAL 2) st 1 <= i & i < width G & i >= width G holds ( b1 = { |[r,s]| where r, s is Real : ( (G * (1,i)) `2 <= s & s <= (G * (1,(i + 1))) `2 ) } iff b1 = { |[r,s]| where r, s is Real : (G * (1,i)) `2 <= s } ); ; end; :: deftheorem Def1 defines v_strip GOBOARD5:def_1_:_ for G being Matrix of (TOP-REAL 2) for i being Nat holds ( ( 1 <= i & i < len G implies v_strip (G,i) = { |[r,s]| where r, s is Real : ( (G * (i,1)) `1 <= r & r <= (G * ((i + 1),1)) `1 ) } ) & ( i >= len G implies v_strip (G,i) = { |[r,s]| where r, s is Real : (G * (i,1)) `1 <= r } ) & ( ( not 1 <= i or not i < len G ) & not i >= len G implies v_strip (G,i) = { |[r,s]| where r, s is Real : r <= (G * ((i + 1),1)) `1 } ) ); :: deftheorem Def2 defines h_strip GOBOARD5:def_2_:_ for G being Matrix of (TOP-REAL 2) for i being Nat holds ( ( 1 <= i & i < width G implies h_strip (G,i) = { |[r,s]| where r, s is Real : ( (G * (1,i)) `2 <= s & s <= (G * (1,(i + 1))) `2 ) } ) & ( i >= width G implies h_strip (G,i) = { |[r,s]| where r, s is Real : (G * (1,i)) `2 <= s } ) & ( ( not 1 <= i or not i < width G ) & not i >= width G implies h_strip (G,i) = { |[r,s]| where r, s is Real : s <= (G * (1,(i + 1))) `2 } ) ); theorem Th1: :: GOBOARD5:1 for j, i being Element of NAT for G being Matrix of (TOP-REAL 2) st G is Y_equal-in-column & 1 <= j & j <= width G & 1 <= i & i <= len G holds (G * (i,j)) `2 = (G * (1,j)) `2 proof let j, i be Element of NAT ; ::_thesis: for G being Matrix of (TOP-REAL 2) st G is Y_equal-in-column & 1 <= j & j <= width G & 1 <= i & i <= len G holds (G * (i,j)) `2 = (G * (1,j)) `2 let G be Matrix of (TOP-REAL 2); ::_thesis: ( G is Y_equal-in-column & 1 <= j & j <= width G & 1 <= i & i <= len G implies (G * (i,j)) `2 = (G * (1,j)) `2 ) assume that A1: G is Y_equal-in-column and A2: 1 <= j and A3: j <= width G and A4: 1 <= i and A5: i <= len G ; ::_thesis: (G * (i,j)) `2 = (G * (1,j)) `2 j in Seg (width G) by A2, A3, FINSEQ_1:1; then A6: Y_axis (Col (G,j)) is constant by A1, GOBOARD1:def_5; reconsider c = Col (G,j) as FinSequence of (TOP-REAL 2) ; A7: i in dom G by A4, A5, FINSEQ_3:25; A8: 1 <= len G by A4, A5, XXREAL_0:2; then A9: 1 in dom G by FINSEQ_3:25; A10: len c = len G by MATRIX_1:def_8; then 1 in dom c by A8, FINSEQ_3:25; then A11: c /. 1 = c . 1 by PARTFUN1:def_6; i in dom c by A4, A5, A10, FINSEQ_3:25; then A12: c /. i = c . i by PARTFUN1:def_6; A13: len (Y_axis (Col (G,j))) = len c by GOBOARD1:def_2; then A14: 1 in dom (Y_axis (Col (G,j))) by A8, A10, FINSEQ_3:25; A15: i in dom (Y_axis (Col (G,j))) by A4, A5, A10, A13, FINSEQ_3:25; thus (G * (i,j)) `2 = (c /. i) `2 by A7, A12, MATRIX_1:def_8 .= (Y_axis (Col (G,j))) . i by A15, GOBOARD1:def_2 .= (Y_axis (Col (G,j))) . 1 by A6, A14, A15, SEQM_3:def_10 .= (c /. 1) `2 by A14, GOBOARD1:def_2 .= (G * (1,j)) `2 by A9, A11, MATRIX_1:def_8 ; ::_thesis: verum end; theorem Th2: :: GOBOARD5:2 for j, i being Element of NAT for G being Matrix of (TOP-REAL 2) st G is X_equal-in-line & 1 <= j & j <= width G & 1 <= i & i <= len G holds (G * (i,j)) `1 = (G * (i,1)) `1 proof let j, i be Element of NAT ; ::_thesis: for G being Matrix of (TOP-REAL 2) st G is X_equal-in-line & 1 <= j & j <= width G & 1 <= i & i <= len G holds (G * (i,j)) `1 = (G * (i,1)) `1 let G be Matrix of (TOP-REAL 2); ::_thesis: ( G is X_equal-in-line & 1 <= j & j <= width G & 1 <= i & i <= len G implies (G * (i,j)) `1 = (G * (i,1)) `1 ) assume that A1: G is X_equal-in-line and A2: 1 <= j and A3: j <= width G and A4: 1 <= i and A5: i <= len G ; ::_thesis: (G * (i,j)) `1 = (G * (i,1)) `1 i in dom G by A4, A5, FINSEQ_3:25; then A6: X_axis (Line (G,i)) is constant by A1, GOBOARD1:def_4; reconsider c = Line (G,i) as FinSequence of (TOP-REAL 2) ; A7: j in Seg (width G) by A2, A3, FINSEQ_1:1; A8: 1 <= width G by A2, A3, XXREAL_0:2; then A9: 1 in Seg (width G) by FINSEQ_1:1; A10: len c = width G by MATRIX_1:def_7; then 1 in dom c by A8, FINSEQ_3:25; then A11: c /. 1 = c . 1 by PARTFUN1:def_6; j in dom c by A2, A3, A10, FINSEQ_3:25; then A12: c /. j = c . j by PARTFUN1:def_6; A13: len (X_axis (Line (G,i))) = len c by GOBOARD1:def_1; then A14: 1 in dom (X_axis (Line (G,i))) by A8, A10, FINSEQ_3:25; A15: j in dom (X_axis (Line (G,i))) by A2, A3, A10, A13, FINSEQ_3:25; thus (G * (i,j)) `1 = (c /. j) `1 by A7, A12, MATRIX_1:def_7 .= (X_axis (Line (G,i))) . j by A15, GOBOARD1:def_1 .= (X_axis (Line (G,i))) . 1 by A6, A14, A15, SEQM_3:def_10 .= (c /. 1) `1 by A14, GOBOARD1:def_1 .= (G * (i,1)) `1 by A9, A11, MATRIX_1:def_7 ; ::_thesis: verum end; theorem Th3: :: GOBOARD5:3 for j, i1, i2 being Element of NAT for G being Matrix of (TOP-REAL 2) st G is X_increasing-in-column & 1 <= j & j <= width G & 1 <= i1 & i1 < i2 & i2 <= len G holds (G * (i1,j)) `1 < (G * (i2,j)) `1 proof let j, i1, i2 be Element of NAT ; ::_thesis: for G being Matrix of (TOP-REAL 2) st G is X_increasing-in-column & 1 <= j & j <= width G & 1 <= i1 & i1 < i2 & i2 <= len G holds (G * (i1,j)) `1 < (G * (i2,j)) `1 let G be Matrix of (TOP-REAL 2); ::_thesis: ( G is X_increasing-in-column & 1 <= j & j <= width G & 1 <= i1 & i1 < i2 & i2 <= len G implies (G * (i1,j)) `1 < (G * (i2,j)) `1 ) assume that A1: G is X_increasing-in-column and A2: 1 <= j and A3: j <= width G and A4: 1 <= i1 and A5: i1 < i2 and A6: i2 <= len G ; ::_thesis: (G * (i1,j)) `1 < (G * (i2,j)) `1 j in Seg (width G) by A2, A3, FINSEQ_1:1; then A7: X_axis (Col (G,j)) is increasing by A1, GOBOARD1:def_7; reconsider c = Col (G,j) as FinSequence of (TOP-REAL 2) ; A8: i1 <= len G by A5, A6, XXREAL_0:2; then A9: i1 in dom G by A4, FINSEQ_3:25; A10: 1 <= i2 by A4, A5, XXREAL_0:2; then A11: i2 in dom G by A6, FINSEQ_3:25; A12: len c = len G by MATRIX_1:def_8; then i1 in dom c by A4, A8, FINSEQ_3:25; then A13: c /. i1 = c . i1 by PARTFUN1:def_6; i2 in dom c by A6, A10, A12, FINSEQ_3:25; then A14: c /. i2 = c . i2 by PARTFUN1:def_6; A15: len (X_axis (Col (G,j))) = len c by GOBOARD1:def_1; then A16: i1 in dom (X_axis (Col (G,j))) by A4, A8, A12, FINSEQ_3:25; A17: (G * (i1,j)) `1 = (c /. i1) `1 by A9, A13, MATRIX_1:def_8 .= (X_axis (Col (G,j))) . i1 by A16, GOBOARD1:def_1 ; A18: i2 in dom (X_axis (Col (G,j))) by A6, A10, A12, A15, FINSEQ_3:25; then (X_axis (Col (G,j))) . i2 = (c /. i2) `1 by GOBOARD1:def_1 .= (G * (i2,j)) `1 by A11, A14, MATRIX_1:def_8 ; hence (G * (i1,j)) `1 < (G * (i2,j)) `1 by A5, A7, A16, A17, A18, SEQM_3:def_1; ::_thesis: verum end; theorem Th4: :: GOBOARD5:4 for j1, j2, i being Element of NAT for G being Matrix of (TOP-REAL 2) st G is Y_increasing-in-line & 1 <= j1 & j1 < j2 & j2 <= width G & 1 <= i & i <= len G holds (G * (i,j1)) `2 < (G * (i,j2)) `2 proof let j1, j2, i be Element of NAT ; ::_thesis: for G being Matrix of (TOP-REAL 2) st G is Y_increasing-in-line & 1 <= j1 & j1 < j2 & j2 <= width G & 1 <= i & i <= len G holds (G * (i,j1)) `2 < (G * (i,j2)) `2 let G be Matrix of (TOP-REAL 2); ::_thesis: ( G is Y_increasing-in-line & 1 <= j1 & j1 < j2 & j2 <= width G & 1 <= i & i <= len G implies (G * (i,j1)) `2 < (G * (i,j2)) `2 ) assume that A1: G is Y_increasing-in-line and A2: 1 <= j1 and A3: j1 < j2 and A4: j2 <= width G and A5: 1 <= i and A6: i <= len G ; ::_thesis: (G * (i,j1)) `2 < (G * (i,j2)) `2 i in dom G by A5, A6, FINSEQ_3:25; then A7: Y_axis (Line (G,i)) is increasing by A1, GOBOARD1:def_6; reconsider c = Line (G,i) as FinSequence of (TOP-REAL 2) ; A8: j1 <= width G by A3, A4, XXREAL_0:2; then A9: j1 in Seg (width G) by A2, FINSEQ_1:1; A10: 1 <= j2 by A2, A3, XXREAL_0:2; then A11: j2 in Seg (width G) by A4, FINSEQ_1:1; A12: len c = width G by MATRIX_1:def_7; then j1 in dom c by A2, A8, FINSEQ_3:25; then A13: c /. j1 = c . j1 by PARTFUN1:def_6; j2 in dom c by A4, A10, A12, FINSEQ_3:25; then A14: c /. j2 = c . j2 by PARTFUN1:def_6; A15: len (Y_axis (Line (G,i))) = len c by GOBOARD1:def_2; then A16: j1 in dom (Y_axis (Line (G,i))) by A2, A8, A12, FINSEQ_3:25; A17: (G * (i,j1)) `2 = (c /. j1) `2 by A9, A13, MATRIX_1:def_7 .= (Y_axis (Line (G,i))) . j1 by A16, GOBOARD1:def_2 ; A18: j2 in dom (Y_axis (Line (G,i))) by A4, A10, A12, A15, FINSEQ_3:25; then (Y_axis (Line (G,i))) . j2 = (c /. j2) `2 by GOBOARD1:def_2 .= (G * (i,j2)) `2 by A11, A14, MATRIX_1:def_7 ; hence (G * (i,j1)) `2 < (G * (i,j2)) `2 by A3, A7, A16, A17, A18, SEQM_3:def_1; ::_thesis: verum end; theorem Th5: :: GOBOARD5:5 for j, i being Element of NAT for G being Matrix of (TOP-REAL 2) st G is Y_equal-in-column & 1 <= j & j < width G & 1 <= i & i <= len G holds h_strip (G,j) = { |[r,s]| where r, s is Real : ( (G * (i,j)) `2 <= s & s <= (G * (i,(j + 1))) `2 ) } proof let j, i be Element of NAT ; ::_thesis: for G being Matrix of (TOP-REAL 2) st G is Y_equal-in-column & 1 <= j & j < width G & 1 <= i & i <= len G holds h_strip (G,j) = { |[r,s]| where r, s is Real : ( (G * (i,j)) `2 <= s & s <= (G * (i,(j + 1))) `2 ) } let G be Matrix of (TOP-REAL 2); ::_thesis: ( G is Y_equal-in-column & 1 <= j & j < width G & 1 <= i & i <= len G implies h_strip (G,j) = { |[r,s]| where r, s is Real : ( (G * (i,j)) `2 <= s & s <= (G * (i,(j + 1))) `2 ) } ) assume that A1: G is Y_equal-in-column and A2: 1 <= j and A3: j < width G and A4: 1 <= i and A5: i <= len G ; ::_thesis: h_strip (G,j) = { |[r,s]| where r, s is Real : ( (G * (i,j)) `2 <= s & s <= (G * (i,(j + 1))) `2 ) } A6: 1 <= j + 1 by A2, NAT_1:13; A7: j + 1 <= width G by A3, NAT_1:13; A8: (G * (i,j)) `2 = (G * (1,j)) `2 by A1, A2, A3, A4, A5, Th1; (G * (i,(j + 1))) `2 = (G * (1,(j + 1))) `2 by A1, A4, A5, A6, A7, Th1; hence h_strip (G,j) = { |[r,s]| where r, s is Real : ( (G * (i,j)) `2 <= s & s <= (G * (i,(j + 1))) `2 ) } by A2, A3, A8, Def2; ::_thesis: verum end; theorem Th6: :: GOBOARD5:6 for i being Element of NAT for G being Matrix of (TOP-REAL 2) st G is V3() & G is Y_equal-in-column & 1 <= i & i <= len G holds h_strip (G,(width G)) = { |[r,s]| where r, s is Real : (G * (i,(width G))) `2 <= s } proof let i be Element of NAT ; ::_thesis: for G being Matrix of (TOP-REAL 2) st G is V3() & G is Y_equal-in-column & 1 <= i & i <= len G holds h_strip (G,(width G)) = { |[r,s]| where r, s is Real : (G * (i,(width G))) `2 <= s } let G be Matrix of (TOP-REAL 2); ::_thesis: ( G is V3() & G is Y_equal-in-column & 1 <= i & i <= len G implies h_strip (G,(width G)) = { |[r,s]| where r, s is Real : (G * (i,(width G))) `2 <= s } ) assume that A1: ( G is V3() & G is Y_equal-in-column ) and A2: 1 <= i and A3: i <= len G ; ::_thesis: h_strip (G,(width G)) = { |[r,s]| where r, s is Real : (G * (i,(width G))) `2 <= s } width G <> 0 by A1, GOBOARD1:def_3; then 1 <= width G by NAT_1:14; then (G * (i,(width G))) `2 = (G * (1,(width G))) `2 by A1, A2, A3, Th1; hence h_strip (G,(width G)) = { |[r,s]| where r, s is Real : (G * (i,(width G))) `2 <= s } by Def2; ::_thesis: verum end; theorem Th7: :: GOBOARD5:7 for i being Element of NAT for G being Matrix of (TOP-REAL 2) st G is V3() & G is Y_equal-in-column & 1 <= i & i <= len G holds h_strip (G,0) = { |[r,s]| where r, s is Real : s <= (G * (i,1)) `2 } proof let i be Element of NAT ; ::_thesis: for G being Matrix of (TOP-REAL 2) st G is V3() & G is Y_equal-in-column & 1 <= i & i <= len G holds h_strip (G,0) = { |[r,s]| where r, s is Real : s <= (G * (i,1)) `2 } let G be Matrix of (TOP-REAL 2); ::_thesis: ( G is V3() & G is Y_equal-in-column & 1 <= i & i <= len G implies h_strip (G,0) = { |[r,s]| where r, s is Real : s <= (G * (i,1)) `2 } ) assume that A1: ( G is V3() & G is Y_equal-in-column ) and A2: 1 <= i and A3: i <= len G ; ::_thesis: h_strip (G,0) = { |[r,s]| where r, s is Real : s <= (G * (i,1)) `2 } set A = { |[r,s]| where r, s is Real : (G * (i,1)) `2 >= s } ; A4: 0 <> width G by A1, GOBOARD1:def_3; then A5: 0 < width G by NAT_1:3; 1 <= width G by A4, NAT_1:14; then (G * (i,1)) `2 = (G * (1,1)) `2 by A1, A2, A3, Th1; then { |[r,s]| where r, s is Real : (G * (i,1)) `2 >= s } = { |[r,s]| where r, s is Real : (G * (1,(1 + 0))) `2 >= s } ; hence h_strip (G,0) = { |[r,s]| where r, s is Real : s <= (G * (i,1)) `2 } by A5, Def2; ::_thesis: verum end; theorem Th8: :: GOBOARD5:8 for i, j being Element of NAT for G being Matrix of (TOP-REAL 2) st G is X_equal-in-line & 1 <= i & i < len G & 1 <= j & j <= width G holds v_strip (G,i) = { |[r,s]| where r, s is Real : ( (G * (i,j)) `1 <= r & r <= (G * ((i + 1),j)) `1 ) } proof let i, j be Element of NAT ; ::_thesis: for G being Matrix of (TOP-REAL 2) st G is X_equal-in-line & 1 <= i & i < len G & 1 <= j & j <= width G holds v_strip (G,i) = { |[r,s]| where r, s is Real : ( (G * (i,j)) `1 <= r & r <= (G * ((i + 1),j)) `1 ) } let G be Matrix of (TOP-REAL 2); ::_thesis: ( G is X_equal-in-line & 1 <= i & i < len G & 1 <= j & j <= width G implies v_strip (G,i) = { |[r,s]| where r, s is Real : ( (G * (i,j)) `1 <= r & r <= (G * ((i + 1),j)) `1 ) } ) assume that A1: G is X_equal-in-line and A2: 1 <= i and A3: i < len G and A4: 1 <= j and A5: j <= width G ; ::_thesis: v_strip (G,i) = { |[r,s]| where r, s is Real : ( (G * (i,j)) `1 <= r & r <= (G * ((i + 1),j)) `1 ) } A6: 1 <= i + 1 by A2, NAT_1:13; A7: i + 1 <= len G by A3, NAT_1:13; A8: (G * (i,j)) `1 = (G * (i,1)) `1 by A1, A2, A3, A4, A5, Th2; (G * ((i + 1),j)) `1 = (G * ((i + 1),1)) `1 by A1, A4, A5, A6, A7, Th2; hence v_strip (G,i) = { |[r,s]| where r, s is Real : ( (G * (i,j)) `1 <= r & r <= (G * ((i + 1),j)) `1 ) } by A2, A3, A8, Def1; ::_thesis: verum end; theorem Th9: :: GOBOARD5:9 for j being Element of NAT for G being Matrix of (TOP-REAL 2) st G is V3() & G is X_equal-in-line & 1 <= j & j <= width G holds v_strip (G,(len G)) = { |[r,s]| where r, s is Real : (G * ((len G),j)) `1 <= r } proof let j be Element of NAT ; ::_thesis: for G being Matrix of (TOP-REAL 2) st G is V3() & G is X_equal-in-line & 1 <= j & j <= width G holds v_strip (G,(len G)) = { |[r,s]| where r, s is Real : (G * ((len G),j)) `1 <= r } let G be Matrix of (TOP-REAL 2); ::_thesis: ( G is V3() & G is X_equal-in-line & 1 <= j & j <= width G implies v_strip (G,(len G)) = { |[r,s]| where r, s is Real : (G * ((len G),j)) `1 <= r } ) assume that A1: ( G is V3() & G is X_equal-in-line ) and A2: 1 <= j and A3: j <= width G ; ::_thesis: v_strip (G,(len G)) = { |[r,s]| where r, s is Real : (G * ((len G),j)) `1 <= r } len G <> 0 by A1, GOBOARD1:def_3; then 1 <= len G by NAT_1:14; then (G * ((len G),j)) `1 = (G * ((len G),1)) `1 by A1, A2, A3, Th2; hence v_strip (G,(len G)) = { |[r,s]| where r, s is Real : (G * ((len G),j)) `1 <= r } by Def1; ::_thesis: verum end; theorem Th10: :: GOBOARD5:10 for j being Element of NAT for G being Matrix of (TOP-REAL 2) st G is V3() & G is X_equal-in-line & 1 <= j & j <= width G holds v_strip (G,0) = { |[r,s]| where r, s is Real : r <= (G * (1,j)) `1 } proof let j be Element of NAT ; ::_thesis: for G being Matrix of (TOP-REAL 2) st G is V3() & G is X_equal-in-line & 1 <= j & j <= width G holds v_strip (G,0) = { |[r,s]| where r, s is Real : r <= (G * (1,j)) `1 } let G be Matrix of (TOP-REAL 2); ::_thesis: ( G is V3() & G is X_equal-in-line & 1 <= j & j <= width G implies v_strip (G,0) = { |[r,s]| where r, s is Real : r <= (G * (1,j)) `1 } ) assume that A1: ( G is V3() & G is X_equal-in-line ) and A2: 1 <= j and A3: j <= width G ; ::_thesis: v_strip (G,0) = { |[r,s]| where r, s is Real : r <= (G * (1,j)) `1 } set A = { |[r,s]| where r, s is Real : (G * (1,j)) `1 >= r } ; A4: 0 <> len G by A1, GOBOARD1:def_3; then A5: 0 < len G by NAT_1:3; 1 <= len G by A4, NAT_1:14; then (G * (1,j)) `1 = (G * (1,1)) `1 by A1, A2, A3, Th2; then { |[r,s]| where r, s is Real : (G * (1,j)) `1 >= r } = { |[r,s]| where r, s is Real : (G * (1,(1 + 0))) `1 >= r } ; hence v_strip (G,0) = { |[r,s]| where r, s is Real : r <= (G * (1,j)) `1 } by A5, Def1; ::_thesis: verum end; definition let G be Matrix of (TOP-REAL 2); let i, j be Nat; func cell (G,i,j) -> Subset of (TOP-REAL 2) equals :: GOBOARD5:def 3 (v_strip (G,i)) /\ (h_strip (G,j)); correctness coherence (v_strip (G,i)) /\ (h_strip (G,j)) is Subset of (TOP-REAL 2); ; end; :: deftheorem defines cell GOBOARD5:def_3_:_ for G being Matrix of (TOP-REAL 2) for i, j being Nat holds cell (G,i,j) = (v_strip (G,i)) /\ (h_strip (G,j)); definition let IT be FinSequence of (TOP-REAL 2); attrIT is s.c.c. means :: GOBOARD5:def 4 for i, j being Element of NAT st i + 1 < j & ( ( i > 1 & j < len IT ) or j + 1 < len IT ) holds LSeg (IT,i) misses LSeg (IT,j); end; :: deftheorem defines s.c.c. GOBOARD5:def_4_:_ for IT being FinSequence of (TOP-REAL 2) holds ( IT is s.c.c. iff for i, j being Element of NAT st i + 1 < j & ( ( i > 1 & j < len IT ) or j + 1 < len IT ) holds LSeg (IT,i) misses LSeg (IT,j) ); definition let IT be non empty FinSequence of (TOP-REAL 2); attrIT is standard means :Def5: :: GOBOARD5:def 5 IT is_sequence_on GoB IT; end; :: deftheorem Def5 defines standard GOBOARD5:def_5_:_ for IT being non empty FinSequence of (TOP-REAL 2) holds ( IT is standard iff IT is_sequence_on GoB IT ); registration clusterV1() V4( NAT ) V5( the carrier of (TOP-REAL 2)) Function-like non constant non empty V33() FinSequence-like FinSubsequence-like circular special unfolded s.c.c. standard for FinSequence of the carrier of (TOP-REAL 2); existence ex b1 being non empty FinSequence of (TOP-REAL 2) st ( not b1 is constant & b1 is special & b1 is unfolded & b1 is circular & b1 is s.c.c. & b1 is standard ) proof set f1 = <*|[0,0]|,|[0,1]|,|[1,1]|*>; set f2 = <*|[1,0]|,|[0,0]|*>; A1: len <*|[0,0]|,|[0,1]|,|[1,1]|*> = 3 by FINSEQ_1:45; A2: len <*|[1,0]|,|[0,0]|*> = 2 by FINSEQ_1:44; then A3: len (<*|[0,0]|,|[0,1]|,|[1,1]|*> ^ <*|[1,0]|,|[0,0]|*>) = 3 + 2 by A1, FINSEQ_1:22; reconsider f = <*|[0,0]|,|[0,1]|,|[1,1]|*> ^ <*|[1,0]|,|[0,0]|*> as non empty FinSequence of (TOP-REAL 2) ; take f ; ::_thesis: ( not f is constant & f is special & f is unfolded & f is circular & f is s.c.c. & f is standard ) A4: 1 in dom <*|[0,0]|,|[0,1]|,|[1,1]|*> by A1, FINSEQ_3:25; then A5: f /. 1 = <*|[0,0]|,|[0,1]|,|[1,1]|*> /. 1 by FINSEQ_4:68 .= |[0,0]| by FINSEQ_4:18 ; A6: 2 in dom <*|[0,0]|,|[0,1]|,|[1,1]|*> by A1, FINSEQ_3:25; then A7: f /. 2 = <*|[0,0]|,|[0,1]|,|[1,1]|*> /. 2 by FINSEQ_4:68 .= |[0,1]| by FINSEQ_4:18 ; A8: dom <*|[0,0]|,|[0,1]|,|[1,1]|*> c= dom f by FINSEQ_1:26; then A9: f . 1 = f /. 1 by A4, PARTFUN1:def_6; f . 2 = f /. 2 by A6, A8, PARTFUN1:def_6; then f . 1 <> f . 2 by A5, A7, A9, SPPOL_2:1; hence not f is constant by A4, A6, A8, SEQM_3:def_10; ::_thesis: ( f is special & f is unfolded & f is circular & f is s.c.c. & f is standard ) 3 in dom <*|[0,0]|,|[0,1]|,|[1,1]|*> by A1, FINSEQ_3:25; then A10: f /. 3 = <*|[0,0]|,|[0,1]|,|[1,1]|*> /. 3 by FINSEQ_4:68 .= |[1,1]| by FINSEQ_4:18 ; 1 in dom <*|[1,0]|,|[0,0]|*> by A2, FINSEQ_3:25; then A11: f /. (3 + 1) = <*|[1,0]|,|[0,0]|*> /. 1 by A1, FINSEQ_4:69 .= |[1,0]| by FINSEQ_4:17 ; 2 in dom <*|[1,0]|,|[0,0]|*> by A2, FINSEQ_3:25; then A12: f /. (3 + 2) = <*|[1,0]|,|[0,0]|*> /. 2 by A1, FINSEQ_4:69 .= |[0,0]| by FINSEQ_4:17 ; 1 + 1 = 2 ; then A13: LSeg (f,1) = LSeg (|[0,0]|,|[0,1]|) by A3, A5, A7, TOPREAL1:def_3; 2 + 1 = 3 ; then A14: LSeg (f,2) = LSeg (|[0,1]|,|[1,1]|) by A3, A7, A10, TOPREAL1:def_3; A15: LSeg (f,3) = LSeg (|[1,1]|,|[1,0]|) by A3, A10, A11, TOPREAL1:def_3; 4 + 1 = 5 ; then A16: LSeg (f,4) = LSeg (|[1,0]|,|[0,0]|) by A3, A11, A12, TOPREAL1:def_3; thus f is special ::_thesis: ( f is unfolded & f is circular & f is s.c.c. & f is standard ) proof let i be Nat; :: according to TOPREAL1:def_5 ::_thesis: ( not 1 <= i or not i + 1 <= len f or (f /. i) `1 = (f /. (i + 1)) `1 or (f /. i) `2 = (f /. (i + 1)) `2 ) assume 1 <= i ; ::_thesis: ( not i + 1 <= len f or (f /. i) `1 = (f /. (i + 1)) `1 or (f /. i) `2 = (f /. (i + 1)) `2 ) then 1 + 1 <= i + 1 by XREAL_1:6; then A17: 1 < i + 1 by XXREAL_0:2; assume i + 1 <= len f ; ::_thesis: ( (f /. i) `1 = (f /. (i + 1)) `1 or (f /. i) `2 = (f /. (i + 1)) `2 ) then A18: ( i + 1 = 1 + 1 or i + 1 = 2 + 1 or i + 1 = 3 + 1 or i + 1 = 4 + 1 ) by A3, A17, NAT_1:29; percases ( i = 1 or i = 2 or i = 3 or i = 4 ) by A18; supposeA19: i = 1 ; ::_thesis: ( (f /. i) `1 = (f /. (i + 1)) `1 or (f /. i) `2 = (f /. (i + 1)) `2 ) (f /. 1) `1 = 0 by A5, EUCLID:52 .= (f /. (1 + 1)) `1 by A7, EUCLID:52 ; hence ( (f /. i) `1 = (f /. (i + 1)) `1 or (f /. i) `2 = (f /. (i + 1)) `2 ) by A19; ::_thesis: verum end; supposeA20: i = 2 ; ::_thesis: ( (f /. i) `1 = (f /. (i + 1)) `1 or (f /. i) `2 = (f /. (i + 1)) `2 ) (f /. 2) `2 = 1 by A7, EUCLID:52 .= (f /. (2 + 1)) `2 by A10, EUCLID:52 ; hence ( (f /. i) `1 = (f /. (i + 1)) `1 or (f /. i) `2 = (f /. (i + 1)) `2 ) by A20; ::_thesis: verum end; supposeA21: i = 3 ; ::_thesis: ( (f /. i) `1 = (f /. (i + 1)) `1 or (f /. i) `2 = (f /. (i + 1)) `2 ) (f /. 3) `1 = 1 by A10, EUCLID:52 .= (f /. (3 + 1)) `1 by A11, EUCLID:52 ; hence ( (f /. i) `1 = (f /. (i + 1)) `1 or (f /. i) `2 = (f /. (i + 1)) `2 ) by A21; ::_thesis: verum end; supposeA22: i = 4 ; ::_thesis: ( (f /. i) `1 = (f /. (i + 1)) `1 or (f /. i) `2 = (f /. (i + 1)) `2 ) (f /. 4) `2 = 0 by A11, EUCLID:52 .= (f /. (4 + 1)) `2 by A12, EUCLID:52 ; hence ( (f /. i) `1 = (f /. (i + 1)) `1 or (f /. i) `2 = (f /. (i + 1)) `2 ) by A22; ::_thesis: verum end; end; end; thus f is unfolded ::_thesis: ( f is circular & f is s.c.c. & f is standard ) proof let i be Nat; :: according to TOPREAL1:def_6 ::_thesis: ( not 1 <= i or not i + 2 <= len f or (LSeg (f,i)) /\ (LSeg (f,(i + 1))) = {(f /. (i + 1))} ) assume 1 <= i ; ::_thesis: ( not i + 2 <= len f or (LSeg (f,i)) /\ (LSeg (f,(i + 1))) = {(f /. (i + 1))} ) then A23: 1 + 2 <= i + 2 by XREAL_1:6; then A24: 2 < i + 2 by XXREAL_0:2; A25: 1 < i + 2 by A23, XXREAL_0:2; assume i + 2 <= len f ; ::_thesis: (LSeg (f,i)) /\ (LSeg (f,(i + 1))) = {(f /. (i + 1))} then A26: ( i + 2 = 1 + 2 or i + 2 = 2 + 2 or i + 2 = 3 + 2 ) by A3, A24, A25, NAT_1:29; percases ( i = 1 or i = 2 or i = 3 ) by A26; suppose i = 1 ; ::_thesis: (LSeg (f,i)) /\ (LSeg (f,(i + 1))) = {(f /. (i + 1))} hence (LSeg (f,i)) /\ (LSeg (f,(i + 1))) = {(f /. (i + 1))} by A3, A5, A7, A14, TOPREAL1:15, TOPREAL1:def_3; ::_thesis: verum end; suppose i = 2 ; ::_thesis: (LSeg (f,i)) /\ (LSeg (f,(i + 1))) = {(f /. (i + 1))} hence (LSeg (f,i)) /\ (LSeg (f,(i + 1))) = {(f /. (i + 1))} by A3, A7, A10, A15, TOPREAL1:18, TOPREAL1:def_3; ::_thesis: verum end; suppose i = 3 ; ::_thesis: (LSeg (f,i)) /\ (LSeg (f,(i + 1))) = {(f /. (i + 1))} hence (LSeg (f,i)) /\ (LSeg (f,(i + 1))) = {(f /. (i + 1))} by A3, A10, A11, A16, TOPREAL1:16, TOPREAL1:def_3; ::_thesis: verum end; end; end; thus f /. 1 = f /. (len f) by A1, A2, A5, A12, FINSEQ_1:22; :: according to FINSEQ_6:def_1 ::_thesis: ( f is s.c.c. & f is standard ) thus f is s.c.c. ::_thesis: f is standard proof let i be Element of NAT ; :: according to GOBOARD5:def_4 ::_thesis: for j being Element of NAT st i + 1 < j & ( ( i > 1 & j < len f ) or j + 1 < len f ) holds LSeg (f,i) misses LSeg (f,j) let j be Element of NAT ; ::_thesis: ( i + 1 < j & ( ( i > 1 & j < len f ) or j + 1 < len f ) implies LSeg (f,i) misses LSeg (f,j) ) assume that A27: i + 1 < j and A28: ( ( i > 1 & j < len f ) or j + 1 < len f ) ; ::_thesis: LSeg (f,i) misses LSeg (f,j) A29: i + 1 >= 1 by NAT_1:11; A30: ( j + 1 = 0 + 1 or j + 1 = 1 + 1 or j + 1 = 2 + 1 or j + 1 = 3 + 1 or j + 1 = 4 + 1 ) by A3, A28, NAT_1:29; A31: (i + 1) + 1 = i + (1 + 1) ; then A32: i + 2 <= j by A27, NAT_1:13; A33: ( i + 2 = 2 + 2 implies i = 2 ) ; A34: ( i + 2 = 1 + 2 implies i = 1 ) ; A35: ( i + 2 = 0 + 2 implies i = 0 ) ; A36: i + 2 <> 0 + 1 by A31; A37: now__::_thesis:_(_(_j_=_2_&_i_=_0_)_or_(_j_=_3_&_(_i_=_0_or_i_=_1_)_)_or_(_j_=_4_&_(_i_=_0_or_i_=_2_)_)_) percases ( j = 2 or j = 3 or j = 4 ) by A27, A29, A30, XXREAL_0:2; case j = 2 ; ::_thesis: i = 0 hence i = 0 by A27, A31, A35, NAT_1:26; ::_thesis: verum end; case j = 3 ; ::_thesis: ( i = 0 or i = 1 ) hence ( i = 0 or i = 1 ) by A27, A31, A34, A35, NAT_1:27; ::_thesis: verum end; case j = 4 ; ::_thesis: ( i = 0 or i = 2 ) hence ( i = 0 or i = 2 ) by A3, A28, A32, A33, A34, A35, A36, NAT_1:28; ::_thesis: verum end; end; end; percases ( i = 0 or ( i = 1 & j = 3 ) or ( i = 2 & j = 4 ) ) by A37; suppose i = 0 ; ::_thesis: LSeg (f,i) misses LSeg (f,j) then LSeg (f,i) = {} by TOPREAL1:def_3; hence (LSeg (f,i)) /\ (LSeg (f,j)) = {} ; :: according to XBOOLE_0:def_7 ::_thesis: verum end; suppose ( i = 1 & j = 3 ) ; ::_thesis: LSeg (f,i) misses LSeg (f,j) hence (LSeg (f,i)) /\ (LSeg (f,j)) = {} by A13, A15, TOPREAL1:20, XBOOLE_0:def_7; :: according to XBOOLE_0:def_7 ::_thesis: verum end; suppose ( i = 2 & j = 4 ) ; ::_thesis: LSeg (f,i) misses LSeg (f,j) hence (LSeg (f,i)) /\ (LSeg (f,j)) = {} by A14, A16, TOPREAL1:19, XBOOLE_0:def_7; :: according to XBOOLE_0:def_7 ::_thesis: verum end; end; end; set Xf1 = <*0,0,1*>; set Xf2 = <*1,0*>; reconsider Xf = <*0,0,1*> ^ <*1,0*> as FinSequence of REAL ; A38: len <*0,0,1*> = 3 by FINSEQ_1:45; A39: len <*1,0*> = 2 by FINSEQ_1:44; then A40: len Xf = 3 + 2 by A38, FINSEQ_1:22; 1 in dom <*0,0,1*> by A38, FINSEQ_3:25; then A41: Xf . 1 = <*0,0,1*> . 1 by FINSEQ_1:def_7 .= 0 by FINSEQ_1:45 ; 2 in dom <*0,0,1*> by A38, FINSEQ_3:25; then A42: Xf . 2 = <*0,0,1*> . 2 by FINSEQ_1:def_7 .= 0 by FINSEQ_1:45 ; 3 in dom <*0,0,1*> by A38, FINSEQ_3:25; then A43: Xf . 3 = <*0,0,1*> . 3 by FINSEQ_1:def_7 .= 1 by FINSEQ_1:45 ; 1 in dom <*1,0*> by A39, FINSEQ_3:25; then A44: Xf . (3 + 1) = <*1,0*> . 1 by A38, FINSEQ_1:def_7 .= 1 by FINSEQ_1:44 ; 2 in dom <*1,0*> by A39, FINSEQ_3:25; then A45: Xf . (3 + 2) = <*1,0*> . 2 by A38, FINSEQ_1:def_7 .= 0 by FINSEQ_1:44 ; now__::_thesis:_for_n_being_Element_of_NAT_st_n_in_dom_Xf_holds_ Xf_._n_=_(f_/._n)_`1 let n be Element of NAT ; ::_thesis: ( n in dom Xf implies Xf . b1 = (f /. b1) `1 ) assume A46: n in dom Xf ; ::_thesis: Xf . b1 = (f /. b1) `1 then A47: n <> 0 by FINSEQ_3:25; A48: n <= 5 by A40, A46, FINSEQ_3:25; percases ( n = 1 or n = 2 or n = 3 or n = 4 or n = 5 ) by A47, A48, NAT_1:29; suppose n = 1 ; ::_thesis: Xf . b1 = (f /. b1) `1 hence Xf . n = (f /. n) `1 by A5, A41, EUCLID:52; ::_thesis: verum end; suppose n = 2 ; ::_thesis: Xf . b1 = (f /. b1) `1 hence Xf . n = (f /. n) `1 by A7, A42, EUCLID:52; ::_thesis: verum end; suppose n = 3 ; ::_thesis: Xf . b1 = (f /. b1) `1 hence Xf . n = (f /. n) `1 by A10, A43, EUCLID:52; ::_thesis: verum end; suppose n = 4 ; ::_thesis: Xf . b1 = (f /. b1) `1 hence Xf . n = (f /. n) `1 by A11, A44, EUCLID:52; ::_thesis: verum end; suppose n = 5 ; ::_thesis: Xf . b1 = (f /. b1) `1 hence Xf . n = (f /. n) `1 by A12, A45, EUCLID:52; ::_thesis: verum end; end; end; then A49: Xf = X_axis f by A3, A40, GOBOARD1:def_1; A50: rng <*0,0,1*> = {0,0,1} by FINSEQ_2:128 .= {0,1} by ENUMSET1:30 ; rng <*1,0*> = {0,1} by FINSEQ_2:127; then A51: rng Xf = {0,1} \/ {0,1} by A50, FINSEQ_1:31 .= {0,1} ; then A52: rng <*0,1*> = rng Xf by FINSEQ_2:127; A53: len <*0,1*> = 2 by FINSEQ_1:44 .= card (rng Xf) by A51, CARD_2:57 ; <*0,1*> is increasing proof let n, m be Element of NAT ; :: according to SEQM_3:def_1 ::_thesis: ( not n in K83(<*0,1*>) or not m in K83(<*0,1*>) or m <= n or not K441(<*0,1*>,m) <= K441(<*0,1*>,n) ) len <*0,1*> = 2 by FINSEQ_1:44; then A54: dom <*0,1*> = {1,2} by FINSEQ_1:2, FINSEQ_1:def_3; assume that A55: n in dom <*0,1*> and A56: m in dom <*0,1*> ; ::_thesis: ( m <= n or not K441(<*0,1*>,m) <= K441(<*0,1*>,n) ) A57: ( n = 1 or n = 2 ) by A54, A55, TARSKI:def_2; A58: ( m = 1 or m = 2 ) by A54, A56, TARSKI:def_2; assume A59: n < m ; ::_thesis: not K441(<*0,1*>,m) <= K441(<*0,1*>,n) then A60: <*0,1*> . n = 0 by A57, A58, FINSEQ_1:44; <*0,1*> . m = 1 by A57, A58, A59, FINSEQ_1:44; hence <*0,1*> . n < <*0,1*> . m by A60; ::_thesis: verum end; then A61: <*0,1*> = Incr (X_axis f) by A49, A52, A53, SEQ_4:def_21; set Yf1 = <*0,1,1*>; set Yf2 = <*0,0*>; reconsider Yf = <*0,1,1*> ^ <*0,0*> as FinSequence of REAL ; A62: len <*0,1,1*> = 3 by FINSEQ_1:45; A63: len <*0,0*> = 2 by FINSEQ_1:44; then A64: len Yf = 3 + 2 by A62, FINSEQ_1:22; 1 in dom <*0,1,1*> by A62, FINSEQ_3:25; then A65: Yf . 1 = <*0,1,1*> . 1 by FINSEQ_1:def_7 .= 0 by FINSEQ_1:45 ; 2 in dom <*0,1,1*> by A62, FINSEQ_3:25; then A66: Yf . 2 = <*0,1,1*> . 2 by FINSEQ_1:def_7 .= 1 by FINSEQ_1:45 ; 3 in dom <*0,1,1*> by A62, FINSEQ_3:25; then A67: Yf . 3 = <*0,1,1*> . 3 by FINSEQ_1:def_7 .= 1 by FINSEQ_1:45 ; 1 in dom <*0,0*> by A63, FINSEQ_3:25; then A68: Yf . (3 + 1) = <*0,0*> . 1 by A62, FINSEQ_1:def_7 .= 0 by FINSEQ_1:44 ; 2 in dom <*0,0*> by A63, FINSEQ_3:25; then A69: Yf . (3 + 2) = <*0,0*> . 2 by A62, FINSEQ_1:def_7 .= 0 by FINSEQ_1:44 ; now__::_thesis:_for_n_being_Element_of_NAT_st_n_in_dom_Yf_holds_ Yf_._n_=_(f_/._n)_`2 let n be Element of NAT ; ::_thesis: ( n in dom Yf implies Yf . b1 = (f /. b1) `2 ) assume A70: n in dom Yf ; ::_thesis: Yf . b1 = (f /. b1) `2 then A71: n <> 0 by FINSEQ_3:25; A72: n <= 5 by A64, A70, FINSEQ_3:25; percases ( n = 1 or n = 2 or n = 3 or n = 4 or n = 5 ) by A71, A72, NAT_1:29; suppose n = 1 ; ::_thesis: Yf . b1 = (f /. b1) `2 hence Yf . n = (f /. n) `2 by A5, A65, EUCLID:52; ::_thesis: verum end; suppose n = 2 ; ::_thesis: Yf . b1 = (f /. b1) `2 hence Yf . n = (f /. n) `2 by A7, A66, EUCLID:52; ::_thesis: verum end; suppose n = 3 ; ::_thesis: Yf . b1 = (f /. b1) `2 hence Yf . n = (f /. n) `2 by A10, A67, EUCLID:52; ::_thesis: verum end; suppose n = 4 ; ::_thesis: Yf . b1 = (f /. b1) `2 hence Yf . n = (f /. n) `2 by A11, A68, EUCLID:52; ::_thesis: verum end; suppose n = 5 ; ::_thesis: Yf . b1 = (f /. b1) `2 hence Yf . n = (f /. n) `2 by A12, A69, EUCLID:52; ::_thesis: verum end; end; end; then A73: Yf = Y_axis f by A3, A64, GOBOARD1:def_2; A74: rng <*0,1,1*> = {0,1,1} by FINSEQ_2:128 .= {1,1,0} by ENUMSET1:59 .= {0,1} by ENUMSET1:30 ; rng <*0,0*> = {0,0} by FINSEQ_2:127 .= {0} by ENUMSET1:29 ; then A75: rng Yf = {0,1} \/ {0} by A74, FINSEQ_1:31 .= {0,0,1} by ENUMSET1:2 .= {0,1} by ENUMSET1:30 ; then A76: rng <*0,1*> = rng Yf by FINSEQ_2:127; A77: len <*0,1*> = 2 by FINSEQ_1:44 .= card (rng Yf) by A75, CARD_2:57 ; <*0,1*> is increasing proof let n, m be Element of NAT ; :: according to SEQM_3:def_1 ::_thesis: ( not n in K83(<*0,1*>) or not m in K83(<*0,1*>) or m <= n or not K441(<*0,1*>,m) <= K441(<*0,1*>,n) ) len <*0,1*> = 2 by FINSEQ_1:44; then A78: dom <*0,1*> = {1,2} by FINSEQ_1:2, FINSEQ_1:def_3; assume that A79: n in dom <*0,1*> and A80: m in dom <*0,1*> ; ::_thesis: ( m <= n or not K441(<*0,1*>,m) <= K441(<*0,1*>,n) ) A81: ( n = 1 or n = 2 ) by A78, A79, TARSKI:def_2; A82: ( m = 1 or m = 2 ) by A78, A80, TARSKI:def_2; assume A83: n < m ; ::_thesis: not K441(<*0,1*>,m) <= K441(<*0,1*>,n) then A84: <*0,1*> . n = 0 by A81, A82, FINSEQ_1:44; <*0,1*> . m = 1 by A81, A82, A83, FINSEQ_1:44; hence <*0,1*> . n < <*0,1*> . m by A84; ::_thesis: verum end; then A85: <*0,1*> = Incr (Y_axis f) by A73, A76, A77, SEQ_4:def_21; set M = (|[0,0]|,|[0,1]|) ][ (|[1,0]|,|[1,1]|); A86: len ((|[0,0]|,|[0,1]|) ][ (|[1,0]|,|[1,1]|)) = 2 by MATRIX_2:3 .= len (Incr (X_axis f)) by A61, FINSEQ_1:44 ; A87: width ((|[0,0]|,|[0,1]|) ][ (|[1,0]|,|[1,1]|)) = 2 by MATRIX_2:3 .= len (Incr (Y_axis f)) by A85, FINSEQ_1:44 ; for n, m being Element of NAT st [n,m] in Indices ((|[0,0]|,|[0,1]|) ][ (|[1,0]|,|[1,1]|)) holds ((|[0,0]|,|[0,1]|) ][ (|[1,0]|,|[1,1]|)) * (n,m) = |[((Incr (X_axis f)) . n),((Incr (Y_axis f)) . m)]| proof let n, m be Element of NAT ; ::_thesis: ( [n,m] in Indices ((|[0,0]|,|[0,1]|) ][ (|[1,0]|,|[1,1]|)) implies ((|[0,0]|,|[0,1]|) ][ (|[1,0]|,|[1,1]|)) * (n,m) = |[((Incr (X_axis f)) . n),((Incr (Y_axis f)) . m)]| ) assume [n,m] in Indices ((|[0,0]|,|[0,1]|) ][ (|[1,0]|,|[1,1]|)) ; ::_thesis: ((|[0,0]|,|[0,1]|) ][ (|[1,0]|,|[1,1]|)) * (n,m) = |[((Incr (X_axis f)) . n),((Incr (Y_axis f)) . m)]| then [n,m] in [:{1,2},{1,2}:] by FINSEQ_1:2, MATRIX_2:3; then A88: [n,m] in {[1,1],[1,2],[2,1],[2,2]} by MCART_1:23; A89: <*0,1*> . 1 = 0 by FINSEQ_1:44; A90: <*0,1*> . 2 = 1 by FINSEQ_1:44; percases ( [n,m] = [1,1] or [n,m] = [1,2] or [n,m] = [2,1] or [n,m] = [2,2] ) by A88, ENUMSET1:def_2; supposeA91: [n,m] = [1,1] ; ::_thesis: ((|[0,0]|,|[0,1]|) ][ (|[1,0]|,|[1,1]|)) * (n,m) = |[((Incr (X_axis f)) . n),((Incr (Y_axis f)) . m)]| then A92: n = 1 by XTUPLE_0:1; m = 1 by A91, XTUPLE_0:1; hence ((|[0,0]|,|[0,1]|) ][ (|[1,0]|,|[1,1]|)) * (n,m) = |[((Incr (X_axis f)) . n),((Incr (Y_axis f)) . m)]| by A61, A85, A89, A92, MATRIX_2:6; ::_thesis: verum end; supposeA93: [n,m] = [1,2] ; ::_thesis: ((|[0,0]|,|[0,1]|) ][ (|[1,0]|,|[1,1]|)) * (n,m) = |[((Incr (X_axis f)) . n),((Incr (Y_axis f)) . m)]| then A94: n = 1 by XTUPLE_0:1; m = 2 by A93, XTUPLE_0:1; hence ((|[0,0]|,|[0,1]|) ][ (|[1,0]|,|[1,1]|)) * (n,m) = |[((Incr (X_axis f)) . n),((Incr (Y_axis f)) . m)]| by A61, A85, A89, A90, A94, MATRIX_2:6; ::_thesis: verum end; supposeA95: [n,m] = [2,1] ; ::_thesis: ((|[0,0]|,|[0,1]|) ][ (|[1,0]|,|[1,1]|)) * (n,m) = |[((Incr (X_axis f)) . n),((Incr (Y_axis f)) . m)]| then A96: n = 2 by XTUPLE_0:1; m = 1 by A95, XTUPLE_0:1; hence ((|[0,0]|,|[0,1]|) ][ (|[1,0]|,|[1,1]|)) * (n,m) = |[((Incr (X_axis f)) . n),((Incr (Y_axis f)) . m)]| by A61, A85, A89, A90, A96, MATRIX_2:6; ::_thesis: verum end; supposeA97: [n,m] = [2,2] ; ::_thesis: ((|[0,0]|,|[0,1]|) ][ (|[1,0]|,|[1,1]|)) * (n,m) = |[((Incr (X_axis f)) . n),((Incr (Y_axis f)) . m)]| then A98: n = 2 by XTUPLE_0:1; m = 2 by A97, XTUPLE_0:1; hence ((|[0,0]|,|[0,1]|) ][ (|[1,0]|,|[1,1]|)) * (n,m) = |[((Incr (X_axis f)) . n),((Incr (Y_axis f)) . m)]| by A61, A85, A90, A98, MATRIX_2:6; ::_thesis: verum end; end; end; then A99: (|[0,0]|,|[0,1]|) ][ (|[1,0]|,|[1,1]|) = GoB ((Incr (X_axis f)),(Incr (Y_axis f))) by A86, A87, GOBOARD2:def_1 .= GoB f by GOBOARD2:def_2 ; then A100: f /. 1 = (GoB f) * (1,1) by A5, MATRIX_2:6; A101: f /. 2 = (GoB f) * (1,2) by A7, A99, MATRIX_2:6; A102: f /. 3 = (GoB f) * (2,2) by A10, A99, MATRIX_2:6; A103: f /. 4 = (GoB f) * (2,1) by A11, A99, MATRIX_2:6; thus for k being Element of NAT st k in dom f holds ex i, j being Element of NAT st ( [i,j] in Indices (GoB f) & f /. k = (GoB f) * (i,j) ) :: according to GOBOARD1:def_9,GOBOARD5:def_5 ::_thesis: for b1 being Element of NAT holds ( not b1 in dom f or not b1 + 1 in dom f or for b2, b3, b4, b5 being Element of NAT holds ( not [b2,b3] in Indices (GoB f) or not [b4,b5] in Indices (GoB f) or not f /. b1 = (GoB f) * (b2,b3) or not f /. (b1 + 1) = (GoB f) * (b4,b5) or (abs (b2 - b4)) + (abs (b3 - b5)) = 1 ) ) proof let k be Element of NAT ; ::_thesis: ( k in dom f implies ex i, j being Element of NAT st ( [i,j] in Indices (GoB f) & f /. k = (GoB f) * (i,j) ) ) assume A104: k in dom f ; ::_thesis: ex i, j being Element of NAT st ( [i,j] in Indices (GoB f) & f /. k = (GoB f) * (i,j) ) then A105: k <= 5 by A3, FINSEQ_3:25; A106: k <> 0 by A104, FINSEQ_3:25; percases ( k = 1 or k = 2 or k = 3 or k = 4 or k = 5 ) by A105, A106, NAT_1:29; supposeA107: k = 1 ; ::_thesis: ex i, j being Element of NAT st ( [i,j] in Indices (GoB f) & f /. k = (GoB f) * (i,j) ) take 1 ; ::_thesis: ex j being Element of NAT st ( [1,j] in Indices (GoB f) & f /. k = (GoB f) * (1,j) ) take 1 ; ::_thesis: ( [1,1] in Indices (GoB f) & f /. k = (GoB f) * (1,1) ) thus [1,1] in Indices (GoB f) by A99, MATRIX_2:4; ::_thesis: f /. k = (GoB f) * (1,1) thus f /. k = (GoB f) * (1,1) by A5, A99, A107, MATRIX_2:6; ::_thesis: verum end; supposeA108: k = 2 ; ::_thesis: ex i, j being Element of NAT st ( [i,j] in Indices (GoB f) & f /. k = (GoB f) * (i,j) ) take 1 ; ::_thesis: ex j being Element of NAT st ( [1,j] in Indices (GoB f) & f /. k = (GoB f) * (1,j) ) take 2 ; ::_thesis: ( [1,2] in Indices (GoB f) & f /. k = (GoB f) * (1,2) ) thus [1,2] in Indices (GoB f) by A99, MATRIX_2:4; ::_thesis: f /. k = (GoB f) * (1,2) thus f /. k = (GoB f) * (1,2) by A7, A99, A108, MATRIX_2:6; ::_thesis: verum end; supposeA109: k = 3 ; ::_thesis: ex i, j being Element of NAT st ( [i,j] in Indices (GoB f) & f /. k = (GoB f) * (i,j) ) take 2 ; ::_thesis: ex j being Element of NAT st ( [2,j] in Indices (GoB f) & f /. k = (GoB f) * (2,j) ) take 2 ; ::_thesis: ( [2,2] in Indices (GoB f) & f /. k = (GoB f) * (2,2) ) thus [2,2] in Indices (GoB f) by A99, MATRIX_2:4; ::_thesis: f /. k = (GoB f) * (2,2) thus f /. k = (GoB f) * (2,2) by A10, A99, A109, MATRIX_2:6; ::_thesis: verum end; supposeA110: k = 4 ; ::_thesis: ex i, j being Element of NAT st ( [i,j] in Indices (GoB f) & f /. k = (GoB f) * (i,j) ) take 2 ; ::_thesis: ex j being Element of NAT st ( [2,j] in Indices (GoB f) & f /. k = (GoB f) * (2,j) ) take 1 ; ::_thesis: ( [2,1] in Indices (GoB f) & f /. k = (GoB f) * (2,1) ) thus [2,1] in Indices (GoB f) by A99, MATRIX_2:4; ::_thesis: f /. k = (GoB f) * (2,1) thus f /. k = (GoB f) * (2,1) by A11, A99, A110, MATRIX_2:6; ::_thesis: verum end; supposeA111: k = 5 ; ::_thesis: ex i, j being Element of NAT st ( [i,j] in Indices (GoB f) & f /. k = (GoB f) * (i,j) ) take 1 ; ::_thesis: ex j being Element of NAT st ( [1,j] in Indices (GoB f) & f /. k = (GoB f) * (1,j) ) take 1 ; ::_thesis: ( [1,1] in Indices (GoB f) & f /. k = (GoB f) * (1,1) ) thus [1,1] in Indices (GoB f) by A99, MATRIX_2:4; ::_thesis: f /. k = (GoB f) * (1,1) thus f /. k = (GoB f) * (1,1) by A12, A99, A111, MATRIX_2:6; ::_thesis: verum end; end; end; let n be Element of NAT ; ::_thesis: ( not n in dom f or not n + 1 in dom f or for b1, b2, b3, b4 being Element of NAT holds ( not [b1,b2] in Indices (GoB f) or not [b3,b4] in Indices (GoB f) or not f /. n = (GoB f) * (b1,b2) or not f /. (n + 1) = (GoB f) * (b3,b4) or (abs (b1 - b3)) + (abs (b2 - b4)) = 1 ) ) assume that A112: n in dom f and A113: n + 1 in dom f ; ::_thesis: for b1, b2, b3, b4 being Element of NAT holds ( not [b1,b2] in Indices (GoB f) or not [b3,b4] in Indices (GoB f) or not f /. n = (GoB f) * (b1,b2) or not f /. (n + 1) = (GoB f) * (b3,b4) or (abs (b1 - b3)) + (abs (b2 - b4)) = 1 ) let m, k, i, j be Element of NAT ; ::_thesis: ( not [m,k] in Indices (GoB f) or not [i,j] in Indices (GoB f) or not f /. n = (GoB f) * (m,k) or not f /. (n + 1) = (GoB f) * (i,j) or (abs (m - i)) + (abs (k - j)) = 1 ) assume that A114: [m,k] in Indices (GoB f) and A115: [i,j] in Indices (GoB f) and A116: f /. n = (GoB f) * (m,k) and A117: f /. (n + 1) = (GoB f) * (i,j) ; ::_thesis: (abs (m - i)) + (abs (k - j)) = 1 A118: n <> 0 by A112, FINSEQ_3:25; n + 1 <= 4 + 1 by A3, A113, FINSEQ_3:25; then A119: n <= 4 by XREAL_1:6; percases ( n = 1 or n = 2 or n = 3 or n = 4 ) by A118, A119, NAT_1:28; supposeA120: n = 1 ; ::_thesis: (abs (m - i)) + (abs (k - j)) = 1 A121: [1,1] in Indices (GoB f) by A99, MATRIX_2:4; then A122: m = 1 by A100, A114, A116, A120, GOBOARD1:5; A123: k = 1 by A100, A114, A116, A120, A121, GOBOARD1:5; A124: [1,2] in Indices (GoB f) by A99, MATRIX_2:4; then A125: i = 1 by A101, A115, A117, A120, GOBOARD1:5; j = 1 + 1 by A101, A115, A117, A120, A124, GOBOARD1:5; then abs (k - j) = 1 by A123, SEQM_3:41; hence (abs (m - i)) + (abs (k - j)) = 1 by A122, A125, SEQM_3:42; ::_thesis: verum end; supposeA126: n = 2 ; ::_thesis: (abs (m - i)) + (abs (k - j)) = 1 A127: [1,2] in Indices (GoB f) by A99, MATRIX_2:4; then A128: m = 1 by A101, A114, A116, A126, GOBOARD1:5; A129: k = 2 by A101, A114, A116, A126, A127, GOBOARD1:5; A130: [2,2] in Indices (GoB f) by A99, MATRIX_2:4; then A131: i = 1 + 1 by A102, A115, A117, A126, GOBOARD1:5; A132: j = 2 by A102, A115, A117, A126, A130, GOBOARD1:5; abs (m - i) = 1 by A128, A131, SEQM_3:41; hence (abs (m - i)) + (abs (k - j)) = 1 by A129, A132, SEQM_3:42; ::_thesis: verum end; supposeA133: n = 3 ; ::_thesis: (abs (m - i)) + (abs (k - j)) = 1 A134: [2,2] in Indices (GoB f) by A99, MATRIX_2:4; then A135: m = 2 by A102, A114, A116, A133, GOBOARD1:5; A136: k = 1 + 1 by A102, A114, A116, A133, A134, GOBOARD1:5; A137: [2,1] in Indices (GoB f) by A99, MATRIX_2:4; then A138: i = 2 by A103, A115, A117, A133, GOBOARD1:5; j = 1 by A103, A115, A117, A133, A137, GOBOARD1:5; then abs (k - j) = 1 by A136, SEQM_3:41; hence (abs (m - i)) + (abs (k - j)) = 1 by A135, A138, SEQM_3:42; ::_thesis: verum end; supposeA139: n = 4 ; ::_thesis: (abs (m - i)) + (abs (k - j)) = 1 A140: [2,1] in Indices (GoB f) by A99, MATRIX_2:4; then A141: m = 1 + 1 by A103, A114, A116, A139, GOBOARD1:5; A142: k = 1 by A103, A114, A116, A139, A140, GOBOARD1:5; A143: [1,1] in Indices (GoB f) by A99, MATRIX_2:4; then A144: i = 1 by A5, A12, A100, A115, A117, A139, GOBOARD1:5; A145: j = 1 by A5, A12, A100, A115, A117, A139, A143, GOBOARD1:5; abs (m - i) = 1 by A141, A144, SEQM_3:41; hence (abs (m - i)) + (abs (k - j)) = 1 by A142, A145, SEQM_3:42; ::_thesis: verum end; end; end; end; Lm1: for f being FinSequence of (TOP-REAL 2) holds dom (X_axis f) = dom f proof let f be FinSequence of (TOP-REAL 2); ::_thesis: dom (X_axis f) = dom f len (X_axis f) = len f by GOBOARD1:def_1; hence dom (X_axis f) = dom f by FINSEQ_3:29; ::_thesis: verum end; Lm2: for f being FinSequence of (TOP-REAL 2) holds dom (Y_axis f) = dom f proof let f be FinSequence of (TOP-REAL 2); ::_thesis: dom (Y_axis f) = dom f len (Y_axis f) = len f by GOBOARD1:def_2; hence dom (Y_axis f) = dom f by FINSEQ_3:29; ::_thesis: verum end; theorem Th11: :: GOBOARD5:11 for f being non empty FinSequence of (TOP-REAL 2) for n being Element of NAT st n in dom f holds ex i, j being Element of NAT st ( [i,j] in Indices (GoB f) & f /. n = (GoB f) * (i,j) ) proof let f be non empty FinSequence of (TOP-REAL 2); ::_thesis: for n being Element of NAT st n in dom f holds ex i, j being Element of NAT st ( [i,j] in Indices (GoB f) & f /. n = (GoB f) * (i,j) ) let n be Element of NAT ; ::_thesis: ( n in dom f implies ex i, j being Element of NAT st ( [i,j] in Indices (GoB f) & f /. n = (GoB f) * (i,j) ) ) assume A1: n in dom f ; ::_thesis: ex i, j being Element of NAT st ( [i,j] in Indices (GoB f) & f /. n = (GoB f) * (i,j) ) A2: GoB f = GoB ((Incr (X_axis f)),(Incr (Y_axis f))) by GOBOARD2:def_2; set x = (f /. n) `1 ; set y = (f /. n) `2 ; A3: n in dom (X_axis f) by A1, Lm1; then (X_axis f) . n = (f /. n) `1 by GOBOARD1:def_1; then (f /. n) `1 in rng (X_axis f) by A3, FUNCT_1:def_3; then (f /. n) `1 in rng (Incr (X_axis f)) by SEQ_4:def_21; then consider i being Nat such that A4: i in dom (Incr (X_axis f)) and A5: (Incr (X_axis f)) . i = (f /. n) `1 by FINSEQ_2:10; A6: n in dom (Y_axis f) by A1, Lm2; then (Y_axis f) . n = (f /. n) `2 by GOBOARD1:def_2; then (f /. n) `2 in rng (Y_axis f) by A6, FUNCT_1:def_3; then (f /. n) `2 in rng (Incr (Y_axis f)) by SEQ_4:def_21; then consider j being Nat such that A7: j in dom (Incr (Y_axis f)) and A8: (Incr (Y_axis f)) . j = (f /. n) `2 by FINSEQ_2:10; reconsider i = i, j = j as Element of NAT by ORDINAL1:def_12; take i ; ::_thesis: ex j being Element of NAT st ( [i,j] in Indices (GoB f) & f /. n = (GoB f) * (i,j) ) take j ; ::_thesis: ( [i,j] in Indices (GoB f) & f /. n = (GoB f) * (i,j) ) i in Seg (len (Incr (X_axis f))) by A4, FINSEQ_1:def_3; then i in Seg (len (GoB ((Incr (X_axis f)),(Incr (Y_axis f))))) by GOBOARD2:def_1; then A9: i in dom (GoB f) by A2, FINSEQ_1:def_3; j in Seg (len (Incr (Y_axis f))) by A7, FINSEQ_1:def_3; then j in Seg (width (GoB ((Incr (X_axis f)),(Incr (Y_axis f))))) by GOBOARD2:def_1; then [i,j] in [:(dom (GoB f)),(Seg (width (GoB f))):] by A2, A9, ZFMISC_1:87; hence A10: [i,j] in Indices (GoB f) by MATRIX_1:def_4; ::_thesis: f /. n = (GoB f) * (i,j) thus f /. n = |[((Incr (X_axis f)) . i),((Incr (Y_axis f)) . j)]| by A5, A8, EUCLID:53 .= (GoB f) * (i,j) by A2, A10, GOBOARD2:def_1 ; ::_thesis: verum end; theorem Th12: :: GOBOARD5:12 for f being non empty standard FinSequence of (TOP-REAL 2) 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 (GoB f) & [i,j] in Indices (GoB f) & f /. n = (GoB f) * (m,k) & f /. (n + 1) = (GoB f) * (i,j) holds (abs (m - i)) + (abs (k - j)) = 1 proof let f be non empty standard FinSequence of (TOP-REAL 2); ::_thesis: 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 (GoB f) & [i,j] in Indices (GoB f) & f /. n = (GoB f) * (m,k) & f /. (n + 1) = (GoB f) * (i,j) holds (abs (m - i)) + (abs (k - j)) = 1 let n be Element of NAT ; ::_thesis: ( n in dom f & n + 1 in dom f implies for m, k, i, j being Element of NAT st [m,k] in Indices (GoB f) & [i,j] in Indices (GoB f) & f /. n = (GoB f) * (m,k) & f /. (n + 1) = (GoB f) * (i,j) holds (abs (m - i)) + (abs (k - j)) = 1 ) assume that A1: n in dom f and A2: n + 1 in dom f ; ::_thesis: for m, k, i, j being Element of NAT st [m,k] in Indices (GoB f) & [i,j] in Indices (GoB f) & f /. n = (GoB f) * (m,k) & f /. (n + 1) = (GoB f) * (i,j) holds (abs (m - i)) + (abs (k - j)) = 1 f is_sequence_on GoB f by Def5; hence for m, k, i, j being Element of NAT st [m,k] in Indices (GoB f) & [i,j] in Indices (GoB f) & f /. n = (GoB f) * (m,k) & f /. (n + 1) = (GoB f) * (i,j) holds (abs (m - i)) + (abs (k - j)) = 1 by A1, A2, GOBOARD1:def_9; ::_thesis: verum end; definition mode special_circular_sequence is non empty circular special unfolded s.c.c. FinSequence of (TOP-REAL 2); end; definition let f be standard special_circular_sequence; let k be Element of NAT ; assume that A1: 1 <= k and A2: k + 1 <= len f ; k <= k + 1 by NAT_1:11; then k <= len f by A2, XXREAL_0:2; then A3: k in dom f by A1, FINSEQ_3:25; then consider i1, j1 being Element of NAT such that A4: [i1,j1] in Indices (GoB f) and A5: f /. k = (GoB f) * (i1,j1) by Th11; k + 1 >= 1 by NAT_1:11; then A6: k + 1 in dom f by A2, FINSEQ_3:25; then consider i2, j2 being Element of NAT such that A7: [i2,j2] in Indices (GoB f) and A8: f /. (k + 1) = (GoB f) * (i2,j2) by Th11; A9: (abs (i1 - i2)) + (abs (j1 - j2)) = 1 by A3, A4, A5, A6, A7, A8, Th12; A10: now__::_thesis:_(_(_abs_(i1_-_i2)_=_1_&_j1_=_j2_&_(_i1_=_i2_+_1_or_i1_+_1_=_i2_)_&_j1_=_j2_)_or_(_i1_=_i2_&_abs_(j1_-_j2)_=_1_&_(_j1_=_j2_+_1_or_j1_+_1_=_j2_)_&_i1_=_i2_)_) percases ( ( abs (i1 - i2) = 1 & j1 = j2 ) or ( i1 = i2 & abs (j1 - j2) = 1 ) ) by A9, SEQM_3:42; casethat A11: abs (i1 - i2) = 1 and A12: j1 = j2 ; ::_thesis: ( ( i1 = i2 + 1 or i1 + 1 = i2 ) & j1 = j2 ) ( i1 - i2 = 1 or - (i1 - i2) = 1 ) by A11, ABSVALUE:def_1; hence ( i1 = i2 + 1 or i1 + 1 = i2 ) ; ::_thesis: j1 = j2 thus j1 = j2 by A12; ::_thesis: verum end; casethat A13: i1 = i2 and A14: abs (j1 - j2) = 1 ; ::_thesis: ( ( j1 = j2 + 1 or j1 + 1 = j2 ) & i1 = i2 ) ( j1 - j2 = 1 or - (j1 - j2) = 1 ) by A14, ABSVALUE:def_1; hence ( j1 = j2 + 1 or j1 + 1 = j2 ) ; ::_thesis: i1 = i2 thus i1 = i2 by A13; ::_thesis: verum end; end; end; func right_cell (f,k) -> Subset of (TOP-REAL 2) means :Def6: :: GOBOARD5:def 6 for i1, j1, i2, j2 being Element of NAT st [i1,j1] in Indices (GoB f) & [i2,j2] in Indices (GoB f) & f /. k = (GoB f) * (i1,j1) & f /. (k + 1) = (GoB f) * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & it = cell ((GoB f),i1,j1) ) & not ( i1 + 1 = i2 & j1 = j2 & it = cell ((GoB f),i1,(j1 -' 1)) ) & not ( i1 = i2 + 1 & j1 = j2 & it = cell ((GoB f),i2,j2) ) holds ( i1 = i2 & j1 = j2 + 1 & it = cell ((GoB f),(i1 -' 1),j2) ); existence ex b1 being Subset of (TOP-REAL 2) st for i1, j1, i2, j2 being Element of NAT st [i1,j1] in Indices (GoB f) & [i2,j2] in Indices (GoB f) & f /. k = (GoB f) * (i1,j1) & f /. (k + 1) = (GoB f) * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & b1 = cell ((GoB f),i1,j1) ) & not ( i1 + 1 = i2 & j1 = j2 & b1 = cell ((GoB f),i1,(j1 -' 1)) ) & not ( i1 = i2 + 1 & j1 = j2 & b1 = cell ((GoB f),i2,j2) ) holds ( i1 = i2 & j1 = j2 + 1 & b1 = cell ((GoB f),(i1 -' 1),j2) ) proof percases ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A10; supposeA15: ( i1 = i2 & j1 + 1 = j2 ) ; ::_thesis: ex b1 being Subset of (TOP-REAL 2) st for i1, j1, i2, j2 being Element of NAT st [i1,j1] in Indices (GoB f) & [i2,j2] in Indices (GoB f) & f /. k = (GoB f) * (i1,j1) & f /. (k + 1) = (GoB f) * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & b1 = cell ((GoB f),i1,j1) ) & not ( i1 + 1 = i2 & j1 = j2 & b1 = cell ((GoB f),i1,(j1 -' 1)) ) & not ( i1 = i2 + 1 & j1 = j2 & b1 = cell ((GoB f),i2,j2) ) holds ( i1 = i2 & j1 = j2 + 1 & b1 = cell ((GoB f),(i1 -' 1),j2) ) take cell ((GoB f),i1,j1) ; ::_thesis: for i1, j1, i2, j2 being Element of NAT st [i1,j1] in Indices (GoB f) & [i2,j2] in Indices (GoB f) & f /. k = (GoB f) * (i1,j1) & f /. (k + 1) = (GoB f) * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & cell ((GoB f),i1,j1) = cell ((GoB f),i1,j1) ) & not ( i1 + 1 = i2 & j1 = j2 & cell ((GoB f),i1,j1) = cell ((GoB f),i1,(j1 -' 1)) ) & not ( i1 = i2 + 1 & j1 = j2 & cell ((GoB f),i1,j1) = cell ((GoB f),i2,j2) ) holds ( i1 = i2 & j1 = j2 + 1 & cell ((GoB f),i1,j1) = cell ((GoB f),(i1 -' 1),j2) ) let i19, j19, i29, j29 be Element of NAT ; ::_thesis: ( [i19,j19] in Indices (GoB f) & [i29,j29] in Indices (GoB f) & f /. k = (GoB f) * (i19,j19) & f /. (k + 1) = (GoB f) * (i29,j29) & not ( i19 = i29 & j19 + 1 = j29 & cell ((GoB f),i1,j1) = cell ((GoB f),i19,j19) ) & not ( i19 + 1 = i29 & j19 = j29 & cell ((GoB f),i1,j1) = cell ((GoB f),i19,(j19 -' 1)) ) & not ( i19 = i29 + 1 & j19 = j29 & cell ((GoB f),i1,j1) = cell ((GoB f),i29,j29) ) implies ( i19 = i29 & j19 = j29 + 1 & cell ((GoB f),i1,j1) = cell ((GoB f),(i19 -' 1),j29) ) ) assume that A16: [i19,j19] in Indices (GoB f) and A17: [i29,j29] in Indices (GoB f) and A18: f /. k = (GoB f) * (i19,j19) and A19: f /. (k + 1) = (GoB f) * (i29,j29) ; ::_thesis: ( ( i19 = i29 & j19 + 1 = j29 & cell ((GoB f),i1,j1) = cell ((GoB f),i19,j19) ) or ( i19 + 1 = i29 & j19 = j29 & cell ((GoB f),i1,j1) = cell ((GoB f),i19,(j19 -' 1)) ) or ( i19 = i29 + 1 & j19 = j29 & cell ((GoB f),i1,j1) = cell ((GoB f),i29,j29) ) or ( i19 = i29 & j19 = j29 + 1 & cell ((GoB f),i1,j1) = cell ((GoB f),(i19 -' 1),j29) ) ) A20: i1 = i19 by A4, A5, A16, A18, GOBOARD1:5; j1 = j19 by A4, A5, A16, A18, GOBOARD1:5; hence ( ( i19 = i29 & j19 + 1 = j29 & cell ((GoB f),i1,j1) = cell ((GoB f),i19,j19) ) or ( i19 + 1 = i29 & j19 = j29 & cell ((GoB f),i1,j1) = cell ((GoB f),i19,(j19 -' 1)) ) or ( i19 = i29 + 1 & j19 = j29 & cell ((GoB f),i1,j1) = cell ((GoB f),i29,j29) ) or ( i19 = i29 & j19 = j29 + 1 & cell ((GoB f),i1,j1) = cell ((GoB f),(i19 -' 1),j29) ) ) by A7, A8, A15, A17, A19, A20, GOBOARD1:5; ::_thesis: verum end; supposeA21: ( i1 + 1 = i2 & j1 = j2 ) ; ::_thesis: ex b1 being Subset of (TOP-REAL 2) st for i1, j1, i2, j2 being Element of NAT st [i1,j1] in Indices (GoB f) & [i2,j2] in Indices (GoB f) & f /. k = (GoB f) * (i1,j1) & f /. (k + 1) = (GoB f) * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & b1 = cell ((GoB f),i1,j1) ) & not ( i1 + 1 = i2 & j1 = j2 & b1 = cell ((GoB f),i1,(j1 -' 1)) ) & not ( i1 = i2 + 1 & j1 = j2 & b1 = cell ((GoB f),i2,j2) ) holds ( i1 = i2 & j1 = j2 + 1 & b1 = cell ((GoB f),(i1 -' 1),j2) ) take cell ((GoB f),i1,(j1 -' 1)) ; ::_thesis: for i1, j1, i2, j2 being Element of NAT st [i1,j1] in Indices (GoB f) & [i2,j2] in Indices (GoB f) & f /. k = (GoB f) * (i1,j1) & f /. (k + 1) = (GoB f) * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & cell ((GoB f),i1,(j1 -' 1)) = cell ((GoB f),i1,j1) ) & not ( i1 + 1 = i2 & j1 = j2 & cell ((GoB f),i1,(j1 -' 1)) = cell ((GoB f),i1,(j1 -' 1)) ) & not ( i1 = i2 + 1 & j1 = j2 & cell ((GoB f),i1,(j1 -' 1)) = cell ((GoB f),i2,j2) ) holds ( i1 = i2 & j1 = j2 + 1 & cell ((GoB f),i1,(j1 -' 1)) = cell ((GoB f),(i1 -' 1),j2) ) let i19, j19, i29, j29 be Element of NAT ; ::_thesis: ( [i19,j19] in Indices (GoB f) & [i29,j29] in Indices (GoB f) & f /. k = (GoB f) * (i19,j19) & f /. (k + 1) = (GoB f) * (i29,j29) & not ( i19 = i29 & j19 + 1 = j29 & cell ((GoB f),i1,(j1 -' 1)) = cell ((GoB f),i19,j19) ) & not ( i19 + 1 = i29 & j19 = j29 & cell ((GoB f),i1,(j1 -' 1)) = cell ((GoB f),i19,(j19 -' 1)) ) & not ( i19 = i29 + 1 & j19 = j29 & cell ((GoB f),i1,(j1 -' 1)) = cell ((GoB f),i29,j29) ) implies ( i19 = i29 & j19 = j29 + 1 & cell ((GoB f),i1,(j1 -' 1)) = cell ((GoB f),(i19 -' 1),j29) ) ) assume that A22: [i19,j19] in Indices (GoB f) and A23: [i29,j29] in Indices (GoB f) and A24: f /. k = (GoB f) * (i19,j19) and A25: f /. (k + 1) = (GoB f) * (i29,j29) ; ::_thesis: ( ( i19 = i29 & j19 + 1 = j29 & cell ((GoB f),i1,(j1 -' 1)) = cell ((GoB f),i19,j19) ) or ( i19 + 1 = i29 & j19 = j29 & cell ((GoB f),i1,(j1 -' 1)) = cell ((GoB f),i19,(j19 -' 1)) ) or ( i19 = i29 + 1 & j19 = j29 & cell ((GoB f),i1,(j1 -' 1)) = cell ((GoB f),i29,j29) ) or ( i19 = i29 & j19 = j29 + 1 & cell ((GoB f),i1,(j1 -' 1)) = cell ((GoB f),(i19 -' 1),j29) ) ) A26: i1 = i19 by A4, A5, A22, A24, GOBOARD1:5; j1 = j19 by A4, A5, A22, A24, GOBOARD1:5; hence ( ( i19 = i29 & j19 + 1 = j29 & cell ((GoB f),i1,(j1 -' 1)) = cell ((GoB f),i19,j19) ) or ( i19 + 1 = i29 & j19 = j29 & cell ((GoB f),i1,(j1 -' 1)) = cell ((GoB f),i19,(j19 -' 1)) ) or ( i19 = i29 + 1 & j19 = j29 & cell ((GoB f),i1,(j1 -' 1)) = cell ((GoB f),i29,j29) ) or ( i19 = i29 & j19 = j29 + 1 & cell ((GoB f),i1,(j1 -' 1)) = cell ((GoB f),(i19 -' 1),j29) ) ) by A7, A8, A21, A23, A25, A26, GOBOARD1:5; ::_thesis: verum end; supposeA27: ( i1 = i2 + 1 & j1 = j2 ) ; ::_thesis: ex b1 being Subset of (TOP-REAL 2) st for i1, j1, i2, j2 being Element of NAT st [i1,j1] in Indices (GoB f) & [i2,j2] in Indices (GoB f) & f /. k = (GoB f) * (i1,j1) & f /. (k + 1) = (GoB f) * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & b1 = cell ((GoB f),i1,j1) ) & not ( i1 + 1 = i2 & j1 = j2 & b1 = cell ((GoB f),i1,(j1 -' 1)) ) & not ( i1 = i2 + 1 & j1 = j2 & b1 = cell ((GoB f),i2,j2) ) holds ( i1 = i2 & j1 = j2 + 1 & b1 = cell ((GoB f),(i1 -' 1),j2) ) take cell ((GoB f),i2,j2) ; ::_thesis: for i1, j1, i2, j2 being Element of NAT st [i1,j1] in Indices (GoB f) & [i2,j2] in Indices (GoB f) & f /. k = (GoB f) * (i1,j1) & f /. (k + 1) = (GoB f) * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & cell ((GoB f),i2,j2) = cell ((GoB f),i1,j1) ) & not ( i1 + 1 = i2 & j1 = j2 & cell ((GoB f),i2,j2) = cell ((GoB f),i1,(j1 -' 1)) ) & not ( i1 = i2 + 1 & j1 = j2 & cell ((GoB f),i2,j2) = cell ((GoB f),i2,j2) ) holds ( i1 = i2 & j1 = j2 + 1 & cell ((GoB f),i2,j2) = cell ((GoB f),(i1 -' 1),j2) ) let i19, j19, i29, j29 be Element of NAT ; ::_thesis: ( [i19,j19] in Indices (GoB f) & [i29,j29] in Indices (GoB f) & f /. k = (GoB f) * (i19,j19) & f /. (k + 1) = (GoB f) * (i29,j29) & not ( i19 = i29 & j19 + 1 = j29 & cell ((GoB f),i2,j2) = cell ((GoB f),i19,j19) ) & not ( i19 + 1 = i29 & j19 = j29 & cell ((GoB f),i2,j2) = cell ((GoB f),i19,(j19 -' 1)) ) & not ( i19 = i29 + 1 & j19 = j29 & cell ((GoB f),i2,j2) = cell ((GoB f),i29,j29) ) implies ( i19 = i29 & j19 = j29 + 1 & cell ((GoB f),i2,j2) = cell ((GoB f),(i19 -' 1),j29) ) ) assume that A28: [i19,j19] in Indices (GoB f) and A29: [i29,j29] in Indices (GoB f) and A30: f /. k = (GoB f) * (i19,j19) and A31: f /. (k + 1) = (GoB f) * (i29,j29) ; ::_thesis: ( ( i19 = i29 & j19 + 1 = j29 & cell ((GoB f),i2,j2) = cell ((GoB f),i19,j19) ) or ( i19 + 1 = i29 & j19 = j29 & cell ((GoB f),i2,j2) = cell ((GoB f),i19,(j19 -' 1)) ) or ( i19 = i29 + 1 & j19 = j29 & cell ((GoB f),i2,j2) = cell ((GoB f),i29,j29) ) or ( i19 = i29 & j19 = j29 + 1 & cell ((GoB f),i2,j2) = cell ((GoB f),(i19 -' 1),j29) ) ) A32: i2 = i29 by A7, A8, A29, A31, GOBOARD1:5; j1 = j19 by A4, A5, A28, A30, GOBOARD1:5; hence ( ( i19 = i29 & j19 + 1 = j29 & cell ((GoB f),i2,j2) = cell ((GoB f),i19,j19) ) or ( i19 + 1 = i29 & j19 = j29 & cell ((GoB f),i2,j2) = cell ((GoB f),i19,(j19 -' 1)) ) or ( i19 = i29 + 1 & j19 = j29 & cell ((GoB f),i2,j2) = cell ((GoB f),i29,j29) ) or ( i19 = i29 & j19 = j29 + 1 & cell ((GoB f),i2,j2) = cell ((GoB f),(i19 -' 1),j29) ) ) by A4, A5, A7, A8, A27, A28, A29, A30, A31, A32, GOBOARD1:5; ::_thesis: verum end; supposeA33: ( i1 = i2 & j1 = j2 + 1 ) ; ::_thesis: ex b1 being Subset of (TOP-REAL 2) st for i1, j1, i2, j2 being Element of NAT st [i1,j1] in Indices (GoB f) & [i2,j2] in Indices (GoB f) & f /. k = (GoB f) * (i1,j1) & f /. (k + 1) = (GoB f) * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & b1 = cell ((GoB f),i1,j1) ) & not ( i1 + 1 = i2 & j1 = j2 & b1 = cell ((GoB f),i1,(j1 -' 1)) ) & not ( i1 = i2 + 1 & j1 = j2 & b1 = cell ((GoB f),i2,j2) ) holds ( i1 = i2 & j1 = j2 + 1 & b1 = cell ((GoB f),(i1 -' 1),j2) ) take cell ((GoB f),(i1 -' 1),j2) ; ::_thesis: for i1, j1, i2, j2 being Element of NAT st [i1,j1] in Indices (GoB f) & [i2,j2] in Indices (GoB f) & f /. k = (GoB f) * (i1,j1) & f /. (k + 1) = (GoB f) * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & cell ((GoB f),(i1 -' 1),j2) = cell ((GoB f),i1,j1) ) & not ( i1 + 1 = i2 & j1 = j2 & cell ((GoB f),(i1 -' 1),j2) = cell ((GoB f),i1,(j1 -' 1)) ) & not ( i1 = i2 + 1 & j1 = j2 & cell ((GoB f),(i1 -' 1),j2) = cell ((GoB f),i2,j2) ) holds ( i1 = i2 & j1 = j2 + 1 & cell ((GoB f),(i1 -' 1),j2) = cell ((GoB f),(i1 -' 1),j2) ) let i19, j19, i29, j29 be Element of NAT ; ::_thesis: ( [i19,j19] in Indices (GoB f) & [i29,j29] in Indices (GoB f) & f /. k = (GoB f) * (i19,j19) & f /. (k + 1) = (GoB f) * (i29,j29) & not ( i19 = i29 & j19 + 1 = j29 & cell ((GoB f),(i1 -' 1),j2) = cell ((GoB f),i19,j19) ) & not ( i19 + 1 = i29 & j19 = j29 & cell ((GoB f),(i1 -' 1),j2) = cell ((GoB f),i19,(j19 -' 1)) ) & not ( i19 = i29 + 1 & j19 = j29 & cell ((GoB f),(i1 -' 1),j2) = cell ((GoB f),i29,j29) ) implies ( i19 = i29 & j19 = j29 + 1 & cell ((GoB f),(i1 -' 1),j2) = cell ((GoB f),(i19 -' 1),j29) ) ) assume that A34: [i19,j19] in Indices (GoB f) and A35: [i29,j29] in Indices (GoB f) and A36: f /. k = (GoB f) * (i19,j19) and A37: f /. (k + 1) = (GoB f) * (i29,j29) ; ::_thesis: ( ( i19 = i29 & j19 + 1 = j29 & cell ((GoB f),(i1 -' 1),j2) = cell ((GoB f),i19,j19) ) or ( i19 + 1 = i29 & j19 = j29 & cell ((GoB f),(i1 -' 1),j2) = cell ((GoB f),i19,(j19 -' 1)) ) or ( i19 = i29 + 1 & j19 = j29 & cell ((GoB f),(i1 -' 1),j2) = cell ((GoB f),i29,j29) ) or ( i19 = i29 & j19 = j29 + 1 & cell ((GoB f),(i1 -' 1),j2) = cell ((GoB f),(i19 -' 1),j29) ) ) A38: i1 = i19 by A4, A5, A34, A36, GOBOARD1:5; j1 = j19 by A4, A5, A34, A36, GOBOARD1:5; hence ( ( i19 = i29 & j19 + 1 = j29 & cell ((GoB f),(i1 -' 1),j2) = cell ((GoB f),i19,j19) ) or ( i19 + 1 = i29 & j19 = j29 & cell ((GoB f),(i1 -' 1),j2) = cell ((GoB f),i19,(j19 -' 1)) ) or ( i19 = i29 + 1 & j19 = j29 & cell ((GoB f),(i1 -' 1),j2) = cell ((GoB f),i29,j29) ) or ( i19 = i29 & j19 = j29 + 1 & cell ((GoB f),(i1 -' 1),j2) = cell ((GoB f),(i19 -' 1),j29) ) ) by A7, A8, A33, A35, A37, A38, GOBOARD1:5; ::_thesis: verum end; end; end; uniqueness for b1, b2 being Subset of (TOP-REAL 2) st ( for i1, j1, i2, j2 being Element of NAT st [i1,j1] in Indices (GoB f) & [i2,j2] in Indices (GoB f) & f /. k = (GoB f) * (i1,j1) & f /. (k + 1) = (GoB f) * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & b1 = cell ((GoB f),i1,j1) ) & not ( i1 + 1 = i2 & j1 = j2 & b1 = cell ((GoB f),i1,(j1 -' 1)) ) & not ( i1 = i2 + 1 & j1 = j2 & b1 = cell ((GoB f),i2,j2) ) holds ( i1 = i2 & j1 = j2 + 1 & b1 = cell ((GoB f),(i1 -' 1),j2) ) ) & ( for i1, j1, i2, j2 being Element of NAT st [i1,j1] in Indices (GoB f) & [i2,j2] in Indices (GoB f) & f /. k = (GoB f) * (i1,j1) & f /. (k + 1) = (GoB f) * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & b2 = cell ((GoB f),i1,j1) ) & not ( i1 + 1 = i2 & j1 = j2 & b2 = cell ((GoB f),i1,(j1 -' 1)) ) & not ( i1 = i2 + 1 & j1 = j2 & b2 = cell ((GoB f),i2,j2) ) holds ( i1 = i2 & j1 = j2 + 1 & b2 = cell ((GoB f),(i1 -' 1),j2) ) ) holds b1 = b2 proof let P1, P2 be Subset of (TOP-REAL 2); ::_thesis: ( ( for i1, j1, i2, j2 being Element of NAT st [i1,j1] in Indices (GoB f) & [i2,j2] in Indices (GoB f) & f /. k = (GoB f) * (i1,j1) & f /. (k + 1) = (GoB f) * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & P1 = cell ((GoB f),i1,j1) ) & not ( i1 + 1 = i2 & j1 = j2 & P1 = cell ((GoB f),i1,(j1 -' 1)) ) & not ( i1 = i2 + 1 & j1 = j2 & P1 = cell ((GoB f),i2,j2) ) holds ( i1 = i2 & j1 = j2 + 1 & P1 = cell ((GoB f),(i1 -' 1),j2) ) ) & ( for i1, j1, i2, j2 being Element of NAT st [i1,j1] in Indices (GoB f) & [i2,j2] in Indices (GoB f) & f /. k = (GoB f) * (i1,j1) & f /. (k + 1) = (GoB f) * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & P2 = cell ((GoB f),i1,j1) ) & not ( i1 + 1 = i2 & j1 = j2 & P2 = cell ((GoB f),i1,(j1 -' 1)) ) & not ( i1 = i2 + 1 & j1 = j2 & P2 = cell ((GoB f),i2,j2) ) holds ( i1 = i2 & j1 = j2 + 1 & P2 = cell ((GoB f),(i1 -' 1),j2) ) ) implies P1 = P2 ) assume that A39: for i1, j1, i2, j2 being Element of NAT st [i1,j1] in Indices (GoB f) & [i2,j2] in Indices (GoB f) & f /. k = (GoB f) * (i1,j1) & f /. (k + 1) = (GoB f) * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & P1 = cell ((GoB f),i1,j1) ) & not ( i1 + 1 = i2 & j1 = j2 & P1 = cell ((GoB f),i1,(j1 -' 1)) ) & not ( i1 = i2 + 1 & j1 = j2 & P1 = cell ((GoB f),i2,j2) ) holds ( i1 = i2 & j1 = j2 + 1 & P1 = cell ((GoB f),(i1 -' 1),j2) ) and A40: for i1, j1, i2, j2 being Element of NAT st [i1,j1] in Indices (GoB f) & [i2,j2] in Indices (GoB f) & f /. k = (GoB f) * (i1,j1) & f /. (k + 1) = (GoB f) * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & P2 = cell ((GoB f),i1,j1) ) & not ( i1 + 1 = i2 & j1 = j2 & P2 = cell ((GoB f),i1,(j1 -' 1)) ) & not ( i1 = i2 + 1 & j1 = j2 & P2 = cell ((GoB f),i2,j2) ) holds ( i1 = i2 & j1 = j2 + 1 & P2 = cell ((GoB f),(i1 -' 1),j2) ) ; ::_thesis: P1 = P2 percases ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A10; suppose ( i1 = i2 & j1 + 1 = j2 ) ; ::_thesis: P1 = P2 then A41: j1 < j2 by XREAL_1:29; A42: j2 <= j2 + 1 by NAT_1:11; hence P1 = cell ((GoB f),i1,j1) by A4, A5, A7, A8, A39, A41 .= P2 by A4, A5, A7, A8, A40, A41, A42 ; ::_thesis: verum end; suppose ( i1 + 1 = i2 & j1 = j2 ) ; ::_thesis: P1 = P2 then A43: i1 < i2 by XREAL_1:29; A44: i2 <= i2 + 1 by NAT_1:11; hence P1 = cell ((GoB f),i1,(j1 -' 1)) by A4, A5, A7, A8, A39, A43 .= P2 by A4, A5, A7, A8, A40, A43, A44 ; ::_thesis: verum end; suppose ( i1 = i2 + 1 & j1 = j2 ) ; ::_thesis: P1 = P2 then A45: i2 < i1 by XREAL_1:29; A46: i1 <= i1 + 1 by NAT_1:11; hence P1 = cell ((GoB f),i2,j2) by A4, A5, A7, A8, A39, A45 .= P2 by A4, A5, A7, A8, A40, A45, A46 ; ::_thesis: verum end; suppose ( i1 = i2 & j1 = j2 + 1 ) ; ::_thesis: P1 = P2 then A47: j2 < j1 by XREAL_1:29; A48: j1 <= j1 + 1 by NAT_1:11; hence P1 = cell ((GoB f),(i1 -' 1),j2) by A4, A5, A7, A8, A39, A47 .= P2 by A4, A5, A7, A8, A40, A47, A48 ; ::_thesis: verum end; end; end; func left_cell (f,k) -> Subset of (TOP-REAL 2) means :Def7: :: GOBOARD5:def 7 for i1, j1, i2, j2 being Element of NAT st [i1,j1] in Indices (GoB f) & [i2,j2] in Indices (GoB f) & f /. k = (GoB f) * (i1,j1) & f /. (k + 1) = (GoB f) * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & it = cell ((GoB f),(i1 -' 1),j1) ) & not ( i1 + 1 = i2 & j1 = j2 & it = cell ((GoB f),i1,j1) ) & not ( i1 = i2 + 1 & j1 = j2 & it = cell ((GoB f),i2,(j2 -' 1)) ) holds ( i1 = i2 & j1 = j2 + 1 & it = cell ((GoB f),i1,j2) ); existence ex b1 being Subset of (TOP-REAL 2) st for i1, j1, i2, j2 being Element of NAT st [i1,j1] in Indices (GoB f) & [i2,j2] in Indices (GoB f) & f /. k = (GoB f) * (i1,j1) & f /. (k + 1) = (GoB f) * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & b1 = cell ((GoB f),(i1 -' 1),j1) ) & not ( i1 + 1 = i2 & j1 = j2 & b1 = cell ((GoB f),i1,j1) ) & not ( i1 = i2 + 1 & j1 = j2 & b1 = cell ((GoB f),i2,(j2 -' 1)) ) holds ( i1 = i2 & j1 = j2 + 1 & b1 = cell ((GoB f),i1,j2) ) proof percases ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A10; supposeA49: ( i1 = i2 & j1 + 1 = j2 ) ; ::_thesis: ex b1 being Subset of (TOP-REAL 2) st for i1, j1, i2, j2 being Element of NAT st [i1,j1] in Indices (GoB f) & [i2,j2] in Indices (GoB f) & f /. k = (GoB f) * (i1,j1) & f /. (k + 1) = (GoB f) * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & b1 = cell ((GoB f),(i1 -' 1),j1) ) & not ( i1 + 1 = i2 & j1 = j2 & b1 = cell ((GoB f),i1,j1) ) & not ( i1 = i2 + 1 & j1 = j2 & b1 = cell ((GoB f),i2,(j2 -' 1)) ) holds ( i1 = i2 & j1 = j2 + 1 & b1 = cell ((GoB f),i1,j2) ) take cell ((GoB f),(i1 -' 1),j1) ; ::_thesis: for i1, j1, i2, j2 being Element of NAT st [i1,j1] in Indices (GoB f) & [i2,j2] in Indices (GoB f) & f /. k = (GoB f) * (i1,j1) & f /. (k + 1) = (GoB f) * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & cell ((GoB f),(i1 -' 1),j1) = cell ((GoB f),(i1 -' 1),j1) ) & not ( i1 + 1 = i2 & j1 = j2 & cell ((GoB f),(i1 -' 1),j1) = cell ((GoB f),i1,j1) ) & not ( i1 = i2 + 1 & j1 = j2 & cell ((GoB f),(i1 -' 1),j1) = cell ((GoB f),i2,(j2 -' 1)) ) holds ( i1 = i2 & j1 = j2 + 1 & cell ((GoB f),(i1 -' 1),j1) = cell ((GoB f),i1,j2) ) let i19, j19, i29, j29 be Element of NAT ; ::_thesis: ( [i19,j19] in Indices (GoB f) & [i29,j29] in Indices (GoB f) & f /. k = (GoB f) * (i19,j19) & f /. (k + 1) = (GoB f) * (i29,j29) & not ( i19 = i29 & j19 + 1 = j29 & cell ((GoB f),(i1 -' 1),j1) = cell ((GoB f),(i19 -' 1),j19) ) & not ( i19 + 1 = i29 & j19 = j29 & cell ((GoB f),(i1 -' 1),j1) = cell ((GoB f),i19,j19) ) & not ( i19 = i29 + 1 & j19 = j29 & cell ((GoB f),(i1 -' 1),j1) = cell ((GoB f),i29,(j29 -' 1)) ) implies ( i19 = i29 & j19 = j29 + 1 & cell ((GoB f),(i1 -' 1),j1) = cell ((GoB f),i19,j29) ) ) assume that A50: [i19,j19] in Indices (GoB f) and A51: [i29,j29] in Indices (GoB f) and A52: f /. k = (GoB f) * (i19,j19) and A53: f /. (k + 1) = (GoB f) * (i29,j29) ; ::_thesis: ( ( i19 = i29 & j19 + 1 = j29 & cell ((GoB f),(i1 -' 1),j1) = cell ((GoB f),(i19 -' 1),j19) ) or ( i19 + 1 = i29 & j19 = j29 & cell ((GoB f),(i1 -' 1),j1) = cell ((GoB f),i19,j19) ) or ( i19 = i29 + 1 & j19 = j29 & cell ((GoB f),(i1 -' 1),j1) = cell ((GoB f),i29,(j29 -' 1)) ) or ( i19 = i29 & j19 = j29 + 1 & cell ((GoB f),(i1 -' 1),j1) = cell ((GoB f),i19,j29) ) ) A54: i1 = i19 by A4, A5, A50, A52, GOBOARD1:5; j1 = j19 by A4, A5, A50, A52, GOBOARD1:5; hence ( ( i19 = i29 & j19 + 1 = j29 & cell ((GoB f),(i1 -' 1),j1) = cell ((GoB f),(i19 -' 1),j19) ) or ( i19 + 1 = i29 & j19 = j29 & cell ((GoB f),(i1 -' 1),j1) = cell ((GoB f),i19,j19) ) or ( i19 = i29 + 1 & j19 = j29 & cell ((GoB f),(i1 -' 1),j1) = cell ((GoB f),i29,(j29 -' 1)) ) or ( i19 = i29 & j19 = j29 + 1 & cell ((GoB f),(i1 -' 1),j1) = cell ((GoB f),i19,j29) ) ) by A7, A8, A49, A51, A53, A54, GOBOARD1:5; ::_thesis: verum end; supposeA55: ( i1 + 1 = i2 & j1 = j2 ) ; ::_thesis: ex b1 being Subset of (TOP-REAL 2) st for i1, j1, i2, j2 being Element of NAT st [i1,j1] in Indices (GoB f) & [i2,j2] in Indices (GoB f) & f /. k = (GoB f) * (i1,j1) & f /. (k + 1) = (GoB f) * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & b1 = cell ((GoB f),(i1 -' 1),j1) ) & not ( i1 + 1 = i2 & j1 = j2 & b1 = cell ((GoB f),i1,j1) ) & not ( i1 = i2 + 1 & j1 = j2 & b1 = cell ((GoB f),i2,(j2 -' 1)) ) holds ( i1 = i2 & j1 = j2 + 1 & b1 = cell ((GoB f),i1,j2) ) take cell ((GoB f),i1,j1) ; ::_thesis: for i1, j1, i2, j2 being Element of NAT st [i1,j1] in Indices (GoB f) & [i2,j2] in Indices (GoB f) & f /. k = (GoB f) * (i1,j1) & f /. (k + 1) = (GoB f) * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & cell ((GoB f),i1,j1) = cell ((GoB f),(i1 -' 1),j1) ) & not ( i1 + 1 = i2 & j1 = j2 & cell ((GoB f),i1,j1) = cell ((GoB f),i1,j1) ) & not ( i1 = i2 + 1 & j1 = j2 & cell ((GoB f),i1,j1) = cell ((GoB f),i2,(j2 -' 1)) ) holds ( i1 = i2 & j1 = j2 + 1 & cell ((GoB f),i1,j1) = cell ((GoB f),i1,j2) ) let i19, j19, i29, j29 be Element of NAT ; ::_thesis: ( [i19,j19] in Indices (GoB f) & [i29,j29] in Indices (GoB f) & f /. k = (GoB f) * (i19,j19) & f /. (k + 1) = (GoB f) * (i29,j29) & not ( i19 = i29 & j19 + 1 = j29 & cell ((GoB f),i1,j1) = cell ((GoB f),(i19 -' 1),j19) ) & not ( i19 + 1 = i29 & j19 = j29 & cell ((GoB f),i1,j1) = cell ((GoB f),i19,j19) ) & not ( i19 = i29 + 1 & j19 = j29 & cell ((GoB f),i1,j1) = cell ((GoB f),i29,(j29 -' 1)) ) implies ( i19 = i29 & j19 = j29 + 1 & cell ((GoB f),i1,j1) = cell ((GoB f),i19,j29) ) ) assume that A56: [i19,j19] in Indices (GoB f) and A57: [i29,j29] in Indices (GoB f) and A58: f /. k = (GoB f) * (i19,j19) and A59: f /. (k + 1) = (GoB f) * (i29,j29) ; ::_thesis: ( ( i19 = i29 & j19 + 1 = j29 & cell ((GoB f),i1,j1) = cell ((GoB f),(i19 -' 1),j19) ) or ( i19 + 1 = i29 & j19 = j29 & cell ((GoB f),i1,j1) = cell ((GoB f),i19,j19) ) or ( i19 = i29 + 1 & j19 = j29 & cell ((GoB f),i1,j1) = cell ((GoB f),i29,(j29 -' 1)) ) or ( i19 = i29 & j19 = j29 + 1 & cell ((GoB f),i1,j1) = cell ((GoB f),i19,j29) ) ) A60: i1 = i19 by A4, A5, A56, A58, GOBOARD1:5; j1 = j19 by A4, A5, A56, A58, GOBOARD1:5; hence ( ( i19 = i29 & j19 + 1 = j29 & cell ((GoB f),i1,j1) = cell ((GoB f),(i19 -' 1),j19) ) or ( i19 + 1 = i29 & j19 = j29 & cell ((GoB f),i1,j1) = cell ((GoB f),i19,j19) ) or ( i19 = i29 + 1 & j19 = j29 & cell ((GoB f),i1,j1) = cell ((GoB f),i29,(j29 -' 1)) ) or ( i19 = i29 & j19 = j29 + 1 & cell ((GoB f),i1,j1) = cell ((GoB f),i19,j29) ) ) by A7, A8, A55, A57, A59, A60, GOBOARD1:5; ::_thesis: verum end; supposeA61: ( i1 = i2 + 1 & j1 = j2 ) ; ::_thesis: ex b1 being Subset of (TOP-REAL 2) st for i1, j1, i2, j2 being Element of NAT st [i1,j1] in Indices (GoB f) & [i2,j2] in Indices (GoB f) & f /. k = (GoB f) * (i1,j1) & f /. (k + 1) = (GoB f) * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & b1 = cell ((GoB f),(i1 -' 1),j1) ) & not ( i1 + 1 = i2 & j1 = j2 & b1 = cell ((GoB f),i1,j1) ) & not ( i1 = i2 + 1 & j1 = j2 & b1 = cell ((GoB f),i2,(j2 -' 1)) ) holds ( i1 = i2 & j1 = j2 + 1 & b1 = cell ((GoB f),i1,j2) ) take cell ((GoB f),i2,(j2 -' 1)) ; ::_thesis: for i1, j1, i2, j2 being Element of NAT st [i1,j1] in Indices (GoB f) & [i2,j2] in Indices (GoB f) & f /. k = (GoB f) * (i1,j1) & f /. (k + 1) = (GoB f) * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & cell ((GoB f),i2,(j2 -' 1)) = cell ((GoB f),(i1 -' 1),j1) ) & not ( i1 + 1 = i2 & j1 = j2 & cell ((GoB f),i2,(j2 -' 1)) = cell ((GoB f),i1,j1) ) & not ( i1 = i2 + 1 & j1 = j2 & cell ((GoB f),i2,(j2 -' 1)) = cell ((GoB f),i2,(j2 -' 1)) ) holds ( i1 = i2 & j1 = j2 + 1 & cell ((GoB f),i2,(j2 -' 1)) = cell ((GoB f),i1,j2) ) let i19, j19, i29, j29 be Element of NAT ; ::_thesis: ( [i19,j19] in Indices (GoB f) & [i29,j29] in Indices (GoB f) & f /. k = (GoB f) * (i19,j19) & f /. (k + 1) = (GoB f) * (i29,j29) & not ( i19 = i29 & j19 + 1 = j29 & cell ((GoB f),i2,(j2 -' 1)) = cell ((GoB f),(i19 -' 1),j19) ) & not ( i19 + 1 = i29 & j19 = j29 & cell ((GoB f),i2,(j2 -' 1)) = cell ((GoB f),i19,j19) ) & not ( i19 = i29 + 1 & j19 = j29 & cell ((GoB f),i2,(j2 -' 1)) = cell ((GoB f),i29,(j29 -' 1)) ) implies ( i19 = i29 & j19 = j29 + 1 & cell ((GoB f),i2,(j2 -' 1)) = cell ((GoB f),i19,j29) ) ) assume that A62: [i19,j19] in Indices (GoB f) and A63: [i29,j29] in Indices (GoB f) and A64: f /. k = (GoB f) * (i19,j19) and A65: f /. (k + 1) = (GoB f) * (i29,j29) ; ::_thesis: ( ( i19 = i29 & j19 + 1 = j29 & cell ((GoB f),i2,(j2 -' 1)) = cell ((GoB f),(i19 -' 1),j19) ) or ( i19 + 1 = i29 & j19 = j29 & cell ((GoB f),i2,(j2 -' 1)) = cell ((GoB f),i19,j19) ) or ( i19 = i29 + 1 & j19 = j29 & cell ((GoB f),i2,(j2 -' 1)) = cell ((GoB f),i29,(j29 -' 1)) ) or ( i19 = i29 & j19 = j29 + 1 & cell ((GoB f),i2,(j2 -' 1)) = cell ((GoB f),i19,j29) ) ) A66: i2 = i29 by A7, A8, A63, A65, GOBOARD1:5; j1 = j19 by A4, A5, A62, A64, GOBOARD1:5; hence ( ( i19 = i29 & j19 + 1 = j29 & cell ((GoB f),i2,(j2 -' 1)) = cell ((GoB f),(i19 -' 1),j19) ) or ( i19 + 1 = i29 & j19 = j29 & cell ((GoB f),i2,(j2 -' 1)) = cell ((GoB f),i19,j19) ) or ( i19 = i29 + 1 & j19 = j29 & cell ((GoB f),i2,(j2 -' 1)) = cell ((GoB f),i29,(j29 -' 1)) ) or ( i19 = i29 & j19 = j29 + 1 & cell ((GoB f),i2,(j2 -' 1)) = cell ((GoB f),i19,j29) ) ) by A4, A5, A7, A8, A61, A62, A63, A64, A65, A66, GOBOARD1:5; ::_thesis: verum end; supposeA67: ( i1 = i2 & j1 = j2 + 1 ) ; ::_thesis: ex b1 being Subset of (TOP-REAL 2) st for i1, j1, i2, j2 being Element of NAT st [i1,j1] in Indices (GoB f) & [i2,j2] in Indices (GoB f) & f /. k = (GoB f) * (i1,j1) & f /. (k + 1) = (GoB f) * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & b1 = cell ((GoB f),(i1 -' 1),j1) ) & not ( i1 + 1 = i2 & j1 = j2 & b1 = cell ((GoB f),i1,j1) ) & not ( i1 = i2 + 1 & j1 = j2 & b1 = cell ((GoB f),i2,(j2 -' 1)) ) holds ( i1 = i2 & j1 = j2 + 1 & b1 = cell ((GoB f),i1,j2) ) take cell ((GoB f),i1,j2) ; ::_thesis: for i1, j1, i2, j2 being Element of NAT st [i1,j1] in Indices (GoB f) & [i2,j2] in Indices (GoB f) & f /. k = (GoB f) * (i1,j1) & f /. (k + 1) = (GoB f) * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & cell ((GoB f),i1,j2) = cell ((GoB f),(i1 -' 1),j1) ) & not ( i1 + 1 = i2 & j1 = j2 & cell ((GoB f),i1,j2) = cell ((GoB f),i1,j1) ) & not ( i1 = i2 + 1 & j1 = j2 & cell ((GoB f),i1,j2) = cell ((GoB f),i2,(j2 -' 1)) ) holds ( i1 = i2 & j1 = j2 + 1 & cell ((GoB f),i1,j2) = cell ((GoB f),i1,j2) ) let i19, j19, i29, j29 be Element of NAT ; ::_thesis: ( [i19,j19] in Indices (GoB f) & [i29,j29] in Indices (GoB f) & f /. k = (GoB f) * (i19,j19) & f /. (k + 1) = (GoB f) * (i29,j29) & not ( i19 = i29 & j19 + 1 = j29 & cell ((GoB f),i1,j2) = cell ((GoB f),(i19 -' 1),j19) ) & not ( i19 + 1 = i29 & j19 = j29 & cell ((GoB f),i1,j2) = cell ((GoB f),i19,j19) ) & not ( i19 = i29 + 1 & j19 = j29 & cell ((GoB f),i1,j2) = cell ((GoB f),i29,(j29 -' 1)) ) implies ( i19 = i29 & j19 = j29 + 1 & cell ((GoB f),i1,j2) = cell ((GoB f),i19,j29) ) ) assume that A68: [i19,j19] in Indices (GoB f) and A69: [i29,j29] in Indices (GoB f) and A70: f /. k = (GoB f) * (i19,j19) and A71: f /. (k + 1) = (GoB f) * (i29,j29) ; ::_thesis: ( ( i19 = i29 & j19 + 1 = j29 & cell ((GoB f),i1,j2) = cell ((GoB f),(i19 -' 1),j19) ) or ( i19 + 1 = i29 & j19 = j29 & cell ((GoB f),i1,j2) = cell ((GoB f),i19,j19) ) or ( i19 = i29 + 1 & j19 = j29 & cell ((GoB f),i1,j2) = cell ((GoB f),i29,(j29 -' 1)) ) or ( i19 = i29 & j19 = j29 + 1 & cell ((GoB f),i1,j2) = cell ((GoB f),i19,j29) ) ) A72: i1 = i19 by A4, A5, A68, A70, GOBOARD1:5; j1 = j19 by A4, A5, A68, A70, GOBOARD1:5; hence ( ( i19 = i29 & j19 + 1 = j29 & cell ((GoB f),i1,j2) = cell ((GoB f),(i19 -' 1),j19) ) or ( i19 + 1 = i29 & j19 = j29 & cell ((GoB f),i1,j2) = cell ((GoB f),i19,j19) ) or ( i19 = i29 + 1 & j19 = j29 & cell ((GoB f),i1,j2) = cell ((GoB f),i29,(j29 -' 1)) ) or ( i19 = i29 & j19 = j29 + 1 & cell ((GoB f),i1,j2) = cell ((GoB f),i19,j29) ) ) by A7, A8, A67, A69, A71, A72, GOBOARD1:5; ::_thesis: verum end; end; end; uniqueness for b1, b2 being Subset of (TOP-REAL 2) st ( for i1, j1, i2, j2 being Element of NAT st [i1,j1] in Indices (GoB f) & [i2,j2] in Indices (GoB f) & f /. k = (GoB f) * (i1,j1) & f /. (k + 1) = (GoB f) * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & b1 = cell ((GoB f),(i1 -' 1),j1) ) & not ( i1 + 1 = i2 & j1 = j2 & b1 = cell ((GoB f),i1,j1) ) & not ( i1 = i2 + 1 & j1 = j2 & b1 = cell ((GoB f),i2,(j2 -' 1)) ) holds ( i1 = i2 & j1 = j2 + 1 & b1 = cell ((GoB f),i1,j2) ) ) & ( for i1, j1, i2, j2 being Element of NAT st [i1,j1] in Indices (GoB f) & [i2,j2] in Indices (GoB f) & f /. k = (GoB f) * (i1,j1) & f /. (k + 1) = (GoB f) * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & b2 = cell ((GoB f),(i1 -' 1),j1) ) & not ( i1 + 1 = i2 & j1 = j2 & b2 = cell ((GoB f),i1,j1) ) & not ( i1 = i2 + 1 & j1 = j2 & b2 = cell ((GoB f),i2,(j2 -' 1)) ) holds ( i1 = i2 & j1 = j2 + 1 & b2 = cell ((GoB f),i1,j2) ) ) holds b1 = b2 proof let P1, P2 be Subset of (TOP-REAL 2); ::_thesis: ( ( for i1, j1, i2, j2 being Element of NAT st [i1,j1] in Indices (GoB f) & [i2,j2] in Indices (GoB f) & f /. k = (GoB f) * (i1,j1) & f /. (k + 1) = (GoB f) * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & P1 = cell ((GoB f),(i1 -' 1),j1) ) & not ( i1 + 1 = i2 & j1 = j2 & P1 = cell ((GoB f),i1,j1) ) & not ( i1 = i2 + 1 & j1 = j2 & P1 = cell ((GoB f),i2,(j2 -' 1)) ) holds ( i1 = i2 & j1 = j2 + 1 & P1 = cell ((GoB f),i1,j2) ) ) & ( for i1, j1, i2, j2 being Element of NAT st [i1,j1] in Indices (GoB f) & [i2,j2] in Indices (GoB f) & f /. k = (GoB f) * (i1,j1) & f /. (k + 1) = (GoB f) * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & P2 = cell ((GoB f),(i1 -' 1),j1) ) & not ( i1 + 1 = i2 & j1 = j2 & P2 = cell ((GoB f),i1,j1) ) & not ( i1 = i2 + 1 & j1 = j2 & P2 = cell ((GoB f),i2,(j2 -' 1)) ) holds ( i1 = i2 & j1 = j2 + 1 & P2 = cell ((GoB f),i1,j2) ) ) implies P1 = P2 ) assume that A73: for i1, j1, i2, j2 being Element of NAT st [i1,j1] in Indices (GoB f) & [i2,j2] in Indices (GoB f) & f /. k = (GoB f) * (i1,j1) & f /. (k + 1) = (GoB f) * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & P1 = cell ((GoB f),(i1 -' 1),j1) ) & not ( i1 + 1 = i2 & j1 = j2 & P1 = cell ((GoB f),i1,j1) ) & not ( i1 = i2 + 1 & j1 = j2 & P1 = cell ((GoB f),i2,(j2 -' 1)) ) holds ( i1 = i2 & j1 = j2 + 1 & P1 = cell ((GoB f),i1,j2) ) and A74: for i1, j1, i2, j2 being Element of NAT st [i1,j1] in Indices (GoB f) & [i2,j2] in Indices (GoB f) & f /. k = (GoB f) * (i1,j1) & f /. (k + 1) = (GoB f) * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & P2 = cell ((GoB f),(i1 -' 1),j1) ) & not ( i1 + 1 = i2 & j1 = j2 & P2 = cell ((GoB f),i1,j1) ) & not ( i1 = i2 + 1 & j1 = j2 & P2 = cell ((GoB f),i2,(j2 -' 1)) ) holds ( i1 = i2 & j1 = j2 + 1 & P2 = cell ((GoB f),i1,j2) ) ; ::_thesis: P1 = P2 percases ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A10; suppose ( i1 = i2 & j1 + 1 = j2 ) ; ::_thesis: P1 = P2 then A75: j1 < j2 by XREAL_1:29; A76: j2 <= j2 + 1 by NAT_1:11; hence P1 = cell ((GoB f),(i1 -' 1),j1) by A4, A5, A7, A8, A73, A75 .= P2 by A4, A5, A7, A8, A74, A75, A76 ; ::_thesis: verum end; suppose ( i1 + 1 = i2 & j1 = j2 ) ; ::_thesis: P1 = P2 then A77: i1 < i2 by XREAL_1:29; A78: i2 <= i2 + 1 by NAT_1:11; hence P1 = cell ((GoB f),i1,j1) by A4, A5, A7, A8, A73, A77 .= P2 by A4, A5, A7, A8, A74, A77, A78 ; ::_thesis: verum end; suppose ( i1 = i2 + 1 & j1 = j2 ) ; ::_thesis: P1 = P2 then A79: i2 < i1 by XREAL_1:29; A80: i1 <= i1 + 1 by NAT_1:11; hence P1 = cell ((GoB f),i2,(j2 -' 1)) by A4, A5, A7, A8, A73, A79 .= P2 by A4, A5, A7, A8, A74, A79, A80 ; ::_thesis: verum end; suppose ( i1 = i2 & j1 = j2 + 1 ) ; ::_thesis: P1 = P2 then A81: j2 < j1 by XREAL_1:29; A82: j1 <= j1 + 1 by NAT_1:11; hence P1 = cell ((GoB f),i1,j2) by A4, A5, A7, A8, A73, A81 .= P2 by A4, A5, A7, A8, A74, A81, A82 ; ::_thesis: verum end; end; end; end; :: deftheorem Def6 defines right_cell GOBOARD5:def_6_:_ for f being standard special_circular_sequence for k being Element of NAT st 1 <= k & k + 1 <= len f holds for b3 being Subset of (TOP-REAL 2) holds ( b3 = right_cell (f,k) iff for i1, j1, i2, j2 being Element of NAT st [i1,j1] in Indices (GoB f) & [i2,j2] in Indices (GoB f) & f /. k = (GoB f) * (i1,j1) & f /. (k + 1) = (GoB f) * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & b3 = cell ((GoB f),i1,j1) ) & not ( i1 + 1 = i2 & j1 = j2 & b3 = cell ((GoB f),i1,(j1 -' 1)) ) & not ( i1 = i2 + 1 & j1 = j2 & b3 = cell ((GoB f),i2,j2) ) holds ( i1 = i2 & j1 = j2 + 1 & b3 = cell ((GoB f),(i1 -' 1),j2) ) ); :: deftheorem Def7 defines left_cell GOBOARD5:def_7_:_ for f being standard special_circular_sequence for k being Element of NAT st 1 <= k & k + 1 <= len f holds for b3 being Subset of (TOP-REAL 2) holds ( b3 = left_cell (f,k) iff for i1, j1, i2, j2 being Element of NAT st [i1,j1] in Indices (GoB f) & [i2,j2] in Indices (GoB f) & f /. k = (GoB f) * (i1,j1) & f /. (k + 1) = (GoB f) * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & b3 = cell ((GoB f),(i1 -' 1),j1) ) & not ( i1 + 1 = i2 & j1 = j2 & b3 = cell ((GoB f),i1,j1) ) & not ( i1 = i2 + 1 & j1 = j2 & b3 = cell ((GoB f),i2,(j2 -' 1)) ) holds ( i1 = i2 & j1 = j2 + 1 & b3 = cell ((GoB f),i1,j2) ) ); theorem Th13: :: GOBOARD5:13 for i, j being Element of NAT for G being Matrix of (TOP-REAL 2) st G is V3() & G is X_equal-in-line & G is X_increasing-in-column & i < len G & 1 <= j & j < width G holds LSeg ((G * ((i + 1),j)),(G * ((i + 1),(j + 1)))) c= v_strip (G,i) proof let i, j be Element of NAT ; ::_thesis: for G being Matrix of (TOP-REAL 2) st G is V3() & G is X_equal-in-line & G is X_increasing-in-column & i < len G & 1 <= j & j < width G holds LSeg ((G * ((i + 1),j)),(G * ((i + 1),(j + 1)))) c= v_strip (G,i) let G be Matrix of (TOP-REAL 2); ::_thesis: ( G is V3() & G is X_equal-in-line & G is X_increasing-in-column & i < len G & 1 <= j & j < width G implies LSeg ((G * ((i + 1),j)),(G * ((i + 1),(j + 1)))) c= v_strip (G,i) ) assume that A1: G is V3() and A2: G is X_equal-in-line and A3: G is X_increasing-in-column and A4: i < len G and A5: 1 <= j and A6: j < width G ; ::_thesis: LSeg ((G * ((i + 1),j)),(G * ((i + 1),(j + 1)))) c= v_strip (G,i) A7: 1 <= j + 1 by A5, NAT_1:13; A8: j + 1 <= width G by A6, NAT_1:13; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in LSeg ((G * ((i + 1),j)),(G * ((i + 1),(j + 1)))) or x in v_strip (G,i) ) assume A9: x in LSeg ((G * ((i + 1),j)),(G * ((i + 1),(j + 1)))) ; ::_thesis: x in v_strip (G,i) then reconsider p = x as Point of (TOP-REAL 2) ; A10: p = |[(p `1),(p `2)]| by EUCLID:53; A11: 1 <= i + 1 by NAT_1:11; A12: i + 1 <= len G by A4, NAT_1:13; then A13: (G * ((i + 1),j)) `1 = (G * ((i + 1),1)) `1 by A2, A5, A6, A11, Th2 .= (G * ((i + 1),(j + 1))) `1 by A2, A7, A8, A11, A12, Th2 ; now__::_thesis:_x_in_v_strip_(G,i) percases ( i = 0 or i > 0 ) by NAT_1:3; supposeA14: i = 0 ; ::_thesis: x in v_strip (G,i) then p `1 <= (G * (1,j)) `1 by A9, A13, TOPREAL1:3; then p in { |[r,s]| where r, s is Real : r <= (G * (1,j)) `1 } by A10; hence x in v_strip (G,i) by A1, A2, A5, A6, A14, Th10; ::_thesis: verum end; suppose i > 0 ; ::_thesis: x in v_strip (G,i) then A15: 0 + 1 <= i by NAT_1:13; A16: (G * ((i + 1),j)) `1 <= p `1 by A9, A13, TOPREAL1:3; A17: p `1 <= (G * ((i + 1),j)) `1 by A9, A13, TOPREAL1:3; then A18: p `1 = (G * ((i + 1),j)) `1 by A16, XXREAL_0:1; i < i + 1 by XREAL_1:29; then (G * (i,j)) `1 < p `1 by A3, A5, A6, A12, A15, A18, Th3; then p in { |[r,s]| where r, s is Real : ( (G * (i,j)) `1 <= r & r <= (G * ((i + 1),j)) `1 ) } by A10, A17; hence x in v_strip (G,i) by A2, A4, A5, A6, A15, Th8; ::_thesis: verum end; end; end; hence x in v_strip (G,i) ; ::_thesis: verum end; theorem Th14: :: GOBOARD5:14 for i, j being Element of NAT for G being Matrix of (TOP-REAL 2) st G is V3() & G is X_equal-in-line & G is X_increasing-in-column & 1 <= i & i <= len G & 1 <= j & j < width G holds LSeg ((G * (i,j)),(G * (i,(j + 1)))) c= v_strip (G,i) proof let i, j be Element of NAT ; ::_thesis: for G being Matrix of (TOP-REAL 2) st G is V3() & G is X_equal-in-line & G is X_increasing-in-column & 1 <= i & i <= len G & 1 <= j & j < width G holds LSeg ((G * (i,j)),(G * (i,(j + 1)))) c= v_strip (G,i) let G be Matrix of (TOP-REAL 2); ::_thesis: ( G is V3() & G is X_equal-in-line & G is X_increasing-in-column & 1 <= i & i <= len G & 1 <= j & j < width G implies LSeg ((G * (i,j)),(G * (i,(j + 1)))) c= v_strip (G,i) ) assume that A1: G is V3() and A2: G is X_equal-in-line and A3: G is X_increasing-in-column and A4: 1 <= i and A5: i <= len G and A6: 1 <= j and A7: j < width G ; ::_thesis: LSeg ((G * (i,j)),(G * (i,(j + 1)))) c= v_strip (G,i) A8: 1 <= j + 1 by A6, NAT_1:13; A9: j + 1 <= width G by A7, NAT_1:13; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in LSeg ((G * (i,j)),(G * (i,(j + 1)))) or x in v_strip (G,i) ) assume A10: x in LSeg ((G * (i,j)),(G * (i,(j + 1)))) ; ::_thesis: x in v_strip (G,i) then reconsider p = x as Point of (TOP-REAL 2) ; A11: p = |[(p `1),(p `2)]| by EUCLID:53; A12: (G * (i,j)) `1 = (G * (i,1)) `1 by A2, A4, A5, A6, A7, Th2 .= (G * (i,(j + 1))) `1 by A2, A4, A5, A8, A9, Th2 ; now__::_thesis:_x_in_v_strip_(G,i) percases ( i = len G or i < len G ) by A5, XXREAL_0:1; supposeA13: i = len G ; ::_thesis: x in v_strip (G,i) then (G * ((len G),j)) `1 <= p `1 by A10, A12, TOPREAL1:3; then p in { |[r,s]| where r, s is Real : (G * ((len G),j)) `1 <= r } by A11; hence x in v_strip (G,i) by A1, A2, A6, A7, A13, Th9; ::_thesis: verum end; supposeA14: i < len G ; ::_thesis: x in v_strip (G,i) then A15: i + 1 <= len G by NAT_1:13; A16: (G * (i,j)) `1 <= p `1 by A10, A12, TOPREAL1:3; p `1 <= (G * (i,j)) `1 by A10, A12, TOPREAL1:3; then A17: p `1 = (G * (i,j)) `1 by A16, XXREAL_0:1; i < i + 1 by XREAL_1:29; then p `1 < (G * ((i + 1),j)) `1 by A3, A4, A6, A7, A15, A17, Th3; then p in { |[r,s]| where r, s is Real : ( (G * (i,j)) `1 <= r & r <= (G * ((i + 1),j)) `1 ) } by A11, A16; hence x in v_strip (G,i) by A2, A4, A6, A7, A14, Th8; ::_thesis: verum end; end; end; hence x in v_strip (G,i) ; ::_thesis: verum end; theorem Th15: :: GOBOARD5:15 for j, i being Element of NAT for G being Matrix of (TOP-REAL 2) st G is V3() & G is Y_equal-in-column & G is Y_increasing-in-line & j < width G & 1 <= i & i < len G holds LSeg ((G * (i,(j + 1))),(G * ((i + 1),(j + 1)))) c= h_strip (G,j) proof let j, i be Element of NAT ; ::_thesis: for G being Matrix of (TOP-REAL 2) st G is V3() & G is Y_equal-in-column & G is Y_increasing-in-line & j < width G & 1 <= i & i < len G holds LSeg ((G * (i,(j + 1))),(G * ((i + 1),(j + 1)))) c= h_strip (G,j) let G be Matrix of (TOP-REAL 2); ::_thesis: ( G is V3() & G is Y_equal-in-column & G is Y_increasing-in-line & j < width G & 1 <= i & i < len G implies LSeg ((G * (i,(j + 1))),(G * ((i + 1),(j + 1)))) c= h_strip (G,j) ) assume that A1: G is V3() and A2: G is Y_equal-in-column and A3: G is Y_increasing-in-line and A4: j < width G and A5: 1 <= i and A6: i < len G ; ::_thesis: LSeg ((G * (i,(j + 1))),(G * ((i + 1),(j + 1)))) c= h_strip (G,j) A7: 1 <= i + 1 by A5, NAT_1:13; A8: i + 1 <= len G by A6, NAT_1:13; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in LSeg ((G * (i,(j + 1))),(G * ((i + 1),(j + 1)))) or x in h_strip (G,j) ) assume A9: x in LSeg ((G * (i,(j + 1))),(G * ((i + 1),(j + 1)))) ; ::_thesis: x in h_strip (G,j) then reconsider p = x as Point of (TOP-REAL 2) ; A10: p = |[(p `1),(p `2)]| by EUCLID:53; A11: 1 <= j + 1 by NAT_1:11; A12: j + 1 <= width G by A4, NAT_1:13; then A13: (G * (i,(j + 1))) `2 = (G * (1,(j + 1))) `2 by A2, A5, A6, A11, Th1 .= (G * ((i + 1),(j + 1))) `2 by A2, A7, A8, A11, A12, Th1 ; now__::_thesis:_x_in_h_strip_(G,j) percases ( j = 0 or j > 0 ) by NAT_1:3; supposeA14: j = 0 ; ::_thesis: x in h_strip (G,j) then p `2 <= (G * (i,1)) `2 by A9, A13, TOPREAL1:4; then p in { |[r,s]| where r, s is Real : s <= (G * (i,1)) `2 } by A10; hence x in h_strip (G,j) by A1, A2, A5, A6, A14, Th7; ::_thesis: verum end; suppose j > 0 ; ::_thesis: x in h_strip (G,j) then A15: 0 + 1 <= j by NAT_1:13; A16: (G * (i,(j + 1))) `2 <= p `2 by A9, A13, TOPREAL1:4; A17: p `2 <= (G * (i,(j + 1))) `2 by A9, A13, TOPREAL1:4; then A18: p `2 = (G * (i,(j + 1))) `2 by A16, XXREAL_0:1; j < j + 1 by XREAL_1:29; then (G * (i,j)) `2 < p `2 by A3, A5, A6, A12, A15, A18, Th4; then p in { |[r,s]| where r, s is Real : ( (G * (i,j)) `2 <= s & s <= (G * (i,(j + 1))) `2 ) } by A10, A17; hence x in h_strip (G,j) by A2, A4, A5, A6, A15, Th5; ::_thesis: verum end; end; end; hence x in h_strip (G,j) ; ::_thesis: verum end; theorem Th16: :: GOBOARD5:16 for j, i being Element of NAT for G being Matrix of (TOP-REAL 2) st G is V3() & G is Y_equal-in-column & G is Y_increasing-in-line & 1 <= j & j <= width G & 1 <= i & i < len G holds LSeg ((G * (i,j)),(G * ((i + 1),j))) c= h_strip (G,j) proof let j, i be Element of NAT ; ::_thesis: for G being Matrix of (TOP-REAL 2) st G is V3() & G is Y_equal-in-column & G is Y_increasing-in-line & 1 <= j & j <= width G & 1 <= i & i < len G holds LSeg ((G * (i,j)),(G * ((i + 1),j))) c= h_strip (G,j) let G be Matrix of (TOP-REAL 2); ::_thesis: ( G is V3() & G is Y_equal-in-column & G is Y_increasing-in-line & 1 <= j & j <= width G & 1 <= i & i < len G implies LSeg ((G * (i,j)),(G * ((i + 1),j))) c= h_strip (G,j) ) assume that A1: G is V3() and A2: G is Y_equal-in-column and A3: G is Y_increasing-in-line and A4: 1 <= j and A5: j <= width G and A6: 1 <= i and A7: i < len G ; ::_thesis: LSeg ((G * (i,j)),(G * ((i + 1),j))) c= h_strip (G,j) A8: 1 <= i + 1 by A6, NAT_1:13; A9: i + 1 <= len G by A7, NAT_1:13; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in LSeg ((G * (i,j)),(G * ((i + 1),j))) or x in h_strip (G,j) ) assume A10: x in LSeg ((G * (i,j)),(G * ((i + 1),j))) ; ::_thesis: x in h_strip (G,j) then reconsider p = x as Point of (TOP-REAL 2) ; A11: p = |[(p `1),(p `2)]| by EUCLID:53; A12: (G * (i,j)) `2 = (G * (1,j)) `2 by A2, A4, A5, A6, A7, Th1 .= (G * ((i + 1),j)) `2 by A2, A4, A5, A8, A9, Th1 ; now__::_thesis:_x_in_h_strip_(G,j) percases ( j = width G or j < width G ) by A5, XXREAL_0:1; supposeA13: j = width G ; ::_thesis: x in h_strip (G,j) then (G * (i,(width G))) `2 <= p `2 by A10, A12, TOPREAL1:4; then p in { |[r,s]| where r, s is Real : (G * (i,(width G))) `2 <= s } by A11; hence x in h_strip (G,j) by A1, A2, A6, A7, A13, Th6; ::_thesis: verum end; supposeA14: j < width G ; ::_thesis: x in h_strip (G,j) then A15: j + 1 <= width G by NAT_1:13; A16: (G * (i,j)) `2 <= p `2 by A10, A12, TOPREAL1:4; p `2 <= (G * (i,j)) `2 by A10, A12, TOPREAL1:4; then A17: p `2 = (G * (i,j)) `2 by A16, XXREAL_0:1; j < j + 1 by XREAL_1:29; then p `2 < (G * (i,(j + 1))) `2 by A3, A4, A6, A7, A15, A17, Th4; then p in { |[r,s]| where r, s is Real : ( (G * (i,j)) `2 <= s & s <= (G * (i,(j + 1))) `2 ) } by A11, A16; hence x in h_strip (G,j) by A2, A4, A6, A7, A14, Th5; ::_thesis: verum end; end; end; hence x in h_strip (G,j) ; ::_thesis: verum end; theorem Th17: :: GOBOARD5:17 for i, j being Element of NAT for G being Matrix of (TOP-REAL 2) st G is Y_equal-in-column & G is Y_increasing-in-line & 1 <= i & i <= len G & 1 <= j & j + 1 <= width G holds LSeg ((G * (i,j)),(G * (i,(j + 1)))) c= h_strip (G,j) proof let i, j be Element of NAT ; ::_thesis: for G being Matrix of (TOP-REAL 2) st G is Y_equal-in-column & G is Y_increasing-in-line & 1 <= i & i <= len G & 1 <= j & j + 1 <= width G holds LSeg ((G * (i,j)),(G * (i,(j + 1)))) c= h_strip (G,j) let G be Matrix of (TOP-REAL 2); ::_thesis: ( G is Y_equal-in-column & G is Y_increasing-in-line & 1 <= i & i <= len G & 1 <= j & j + 1 <= width G implies LSeg ((G * (i,j)),(G * (i,(j + 1)))) c= h_strip (G,j) ) assume that A1: G is Y_equal-in-column and A2: G is Y_increasing-in-line and A3: 1 <= i and A4: i <= len G and A5: 1 <= j and A6: j + 1 <= width G ; ::_thesis: LSeg ((G * (i,j)),(G * (i,(j + 1)))) c= h_strip (G,j) let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in LSeg ((G * (i,j)),(G * (i,(j + 1)))) or x in h_strip (G,j) ) assume A7: x in LSeg ((G * (i,j)),(G * (i,(j + 1)))) ; ::_thesis: x in h_strip (G,j) then reconsider p = x as Point of (TOP-REAL 2) ; A8: p = |[(p `1),(p `2)]| by EUCLID:53; A9: j < width G by A6, NAT_1:13; j < j + 1 by XREAL_1:29; then A10: (G * (i,j)) `2 < (G * (i,(j + 1))) `2 by A2, A3, A4, A5, A6, Th4; then A11: (G * (i,j)) `2 <= p `2 by A7, TOPREAL1:4; p `2 <= (G * (i,(j + 1))) `2 by A7, A10, TOPREAL1:4; then p in { |[r,s]| where r, s is Real : ( (G * (i,j)) `2 <= s & s <= (G * (i,(j + 1))) `2 ) } by A8, A11; hence x in h_strip (G,j) by A1, A3, A4, A5, A9, Th5; ::_thesis: verum end; theorem Th18: :: GOBOARD5:18 for i, j being Element of NAT for G being Go-board st i < len G & 1 <= j & j < width G holds LSeg ((G * ((i + 1),j)),(G * ((i + 1),(j + 1)))) c= cell (G,i,j) proof let i, j be Element of NAT ; ::_thesis: for G being Go-board st i < len G & 1 <= j & j < width G holds LSeg ((G * ((i + 1),j)),(G * ((i + 1),(j + 1)))) c= cell (G,i,j) let G be Go-board; ::_thesis: ( i < len G & 1 <= j & j < width G implies LSeg ((G * ((i + 1),j)),(G * ((i + 1),(j + 1)))) c= cell (G,i,j) ) assume that A1: i < len G and A2: 1 <= j and A3: j < width G ; ::_thesis: LSeg ((G * ((i + 1),j)),(G * ((i + 1),(j + 1)))) c= cell (G,i,j) A4: LSeg ((G * ((i + 1),j)),(G * ((i + 1),(j + 1)))) c= v_strip (G,i) by A1, A2, A3, Th13; A5: 1 <= i + 1 by NAT_1:11; A6: i + 1 <= len G by A1, NAT_1:13; j + 1 <= width G by A3, NAT_1:13; then LSeg ((G * ((i + 1),j)),(G * ((i + 1),(j + 1)))) c= h_strip (G,j) by A2, A5, A6, Th17; hence LSeg ((G * ((i + 1),j)),(G * ((i + 1),(j + 1)))) c= cell (G,i,j) by A4, XBOOLE_1:19; ::_thesis: verum end; theorem Th19: :: GOBOARD5:19 for i, j being Element of NAT for G being Go-board st 1 <= i & i <= len G & 1 <= j & j < width G holds LSeg ((G * (i,j)),(G * (i,(j + 1)))) c= cell (G,i,j) proof let i, j be Element of NAT ; ::_thesis: for G being Go-board st 1 <= i & i <= len G & 1 <= j & j < width G holds LSeg ((G * (i,j)),(G * (i,(j + 1)))) c= cell (G,i,j) let G be Go-board; ::_thesis: ( 1 <= i & i <= len G & 1 <= j & j < width G implies LSeg ((G * (i,j)),(G * (i,(j + 1)))) c= cell (G,i,j) ) assume that A1: 1 <= i and A2: i <= len G and A3: 1 <= j and A4: j < width G ; ::_thesis: LSeg ((G * (i,j)),(G * (i,(j + 1)))) c= cell (G,i,j) A5: LSeg ((G * (i,j)),(G * (i,(j + 1)))) c= v_strip (G,i) by A1, A2, A3, A4, Th14; j + 1 <= width G by A4, NAT_1:13; then LSeg ((G * (i,j)),(G * (i,(j + 1)))) c= h_strip (G,j) by A1, A2, A3, Th17; hence LSeg ((G * (i,j)),(G * (i,(j + 1)))) c= cell (G,i,j) by A5, XBOOLE_1:19; ::_thesis: verum end; theorem Th20: :: GOBOARD5:20 for j, i being Element of NAT for G being Matrix of (TOP-REAL 2) st G is X_equal-in-line & G is X_increasing-in-column & 1 <= j & j <= width G & 1 <= i & i + 1 <= len G holds LSeg ((G * (i,j)),(G * ((i + 1),j))) c= v_strip (G,i) proof let j, i be Element of NAT ; ::_thesis: for G being Matrix of (TOP-REAL 2) st G is X_equal-in-line & G is X_increasing-in-column & 1 <= j & j <= width G & 1 <= i & i + 1 <= len G holds LSeg ((G * (i,j)),(G * ((i + 1),j))) c= v_strip (G,i) let G be Matrix of (TOP-REAL 2); ::_thesis: ( G is X_equal-in-line & G is X_increasing-in-column & 1 <= j & j <= width G & 1 <= i & i + 1 <= len G implies LSeg ((G * (i,j)),(G * ((i + 1),j))) c= v_strip (G,i) ) assume that A1: G is X_equal-in-line and A2: G is X_increasing-in-column and A3: 1 <= j and A4: j <= width G and A5: 1 <= i and A6: i + 1 <= len G ; ::_thesis: LSeg ((G * (i,j)),(G * ((i + 1),j))) c= v_strip (G,i) let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in LSeg ((G * (i,j)),(G * ((i + 1),j))) or x in v_strip (G,i) ) assume A7: x in LSeg ((G * (i,j)),(G * ((i + 1),j))) ; ::_thesis: x in v_strip (G,i) then reconsider p = x as Point of (TOP-REAL 2) ; A8: p = |[(p `1),(p `2)]| by EUCLID:53; A9: i < len G by A6, NAT_1:13; i < i + 1 by XREAL_1:29; then A10: (G * (i,j)) `1 < (G * ((i + 1),j)) `1 by A2, A3, A4, A5, A6, Th3; then A11: (G * (i,j)) `1 <= p `1 by A7, TOPREAL1:3; p `1 <= (G * ((i + 1),j)) `1 by A7, A10, TOPREAL1:3; then p in { |[r,s]| where r, s is Real : ( (G * (i,j)) `1 <= r & r <= (G * ((i + 1),j)) `1 ) } by A8, A11; hence x in v_strip (G,i) by A1, A3, A4, A5, A9, Th8; ::_thesis: verum end; theorem Th21: :: GOBOARD5:21 for j, i being Element of NAT for G being Go-board st j < width G & 1 <= i & i < len G holds LSeg ((G * (i,(j + 1))),(G * ((i + 1),(j + 1)))) c= cell (G,i,j) proof let j, i be Element of NAT ; ::_thesis: for G being Go-board st j < width G & 1 <= i & i < len G holds LSeg ((G * (i,(j + 1))),(G * ((i + 1),(j + 1)))) c= cell (G,i,j) let G be Go-board; ::_thesis: ( j < width G & 1 <= i & i < len G implies LSeg ((G * (i,(j + 1))),(G * ((i + 1),(j + 1)))) c= cell (G,i,j) ) assume that A1: j < width G and A2: 1 <= i and A3: i < len G ; ::_thesis: LSeg ((G * (i,(j + 1))),(G * ((i + 1),(j + 1)))) c= cell (G,i,j) A4: LSeg ((G * (i,(j + 1))),(G * ((i + 1),(j + 1)))) c= h_strip (G,j) by A1, A2, A3, Th15; A5: 1 <= j + 1 by NAT_1:11; A6: i + 1 <= len G by A3, NAT_1:13; j + 1 <= width G by A1, NAT_1:13; then LSeg ((G * (i,(j + 1))),(G * ((i + 1),(j + 1)))) c= v_strip (G,i) by A2, A5, A6, Th20; hence LSeg ((G * (i,(j + 1))),(G * ((i + 1),(j + 1)))) c= cell (G,i,j) by A4, XBOOLE_1:19; ::_thesis: verum end; theorem Th22: :: GOBOARD5:22 for i, j being Element of NAT for G being Go-board st 1 <= i & i < len G & 1 <= j & j <= width G holds LSeg ((G * (i,j)),(G * ((i + 1),j))) c= cell (G,i,j) proof let i, j be Element of NAT ; ::_thesis: for G being Go-board st 1 <= i & i < len G & 1 <= j & j <= width G holds LSeg ((G * (i,j)),(G * ((i + 1),j))) c= cell (G,i,j) let G be Go-board; ::_thesis: ( 1 <= i & i < len G & 1 <= j & j <= width G implies LSeg ((G * (i,j)),(G * ((i + 1),j))) c= cell (G,i,j) ) assume that A1: 1 <= i and A2: i < len G and A3: 1 <= j and A4: j <= width G ; ::_thesis: LSeg ((G * (i,j)),(G * ((i + 1),j))) c= cell (G,i,j) A5: LSeg ((G * (i,j)),(G * ((i + 1),j))) c= h_strip (G,j) by A1, A2, A3, A4, Th16; i + 1 <= len G by A2, NAT_1:13; then LSeg ((G * (i,j)),(G * ((i + 1),j))) c= v_strip (G,i) by A1, A3, A4, Th20; hence LSeg ((G * (i,j)),(G * ((i + 1),j))) c= cell (G,i,j) by A5, XBOOLE_1:19; ::_thesis: verum end; theorem Th23: :: GOBOARD5:23 for i being Element of NAT for G being Matrix of (TOP-REAL 2) st G is V3() & G is X_equal-in-line & G is X_increasing-in-column & i + 1 <= len G holds (v_strip (G,i)) /\ (v_strip (G,(i + 1))) = { q where q is Point of (TOP-REAL 2) : q `1 = (G * ((i + 1),1)) `1 } proof let i be Element of NAT ; ::_thesis: for G being Matrix of (TOP-REAL 2) st G is V3() & G is X_equal-in-line & G is X_increasing-in-column & i + 1 <= len G holds (v_strip (G,i)) /\ (v_strip (G,(i + 1))) = { q where q is Point of (TOP-REAL 2) : q `1 = (G * ((i + 1),1)) `1 } let G be Matrix of (TOP-REAL 2); ::_thesis: ( G is V3() & G is X_equal-in-line & G is X_increasing-in-column & i + 1 <= len G implies (v_strip (G,i)) /\ (v_strip (G,(i + 1))) = { q where q is Point of (TOP-REAL 2) : q `1 = (G * ((i + 1),1)) `1 } ) assume that A1: ( G is V3() & G is X_equal-in-line ) and A2: G is X_increasing-in-column and A3: i + 1 <= len G ; ::_thesis: (v_strip (G,i)) /\ (v_strip (G,(i + 1))) = { q where q is Point of (TOP-REAL 2) : q `1 = (G * ((i + 1),1)) `1 } width G <> 0 by A1, GOBOARD1:def_3; then A4: 1 <= width G by NAT_1:14; A5: i < len G by A3, NAT_1:13; thus (v_strip (G,i)) /\ (v_strip (G,(i + 1))) c= { q where q is Point of (TOP-REAL 2) : q `1 = (G * ((i + 1),1)) `1 } :: according to XBOOLE_0:def_10 ::_thesis: { q where q is Point of (TOP-REAL 2) : q `1 = (G * ((i + 1),1)) `1 } c= (v_strip (G,i)) /\ (v_strip (G,(i + 1))) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (v_strip (G,i)) /\ (v_strip (G,(i + 1))) or x in { q where q is Point of (TOP-REAL 2) : q `1 = (G * ((i + 1),1)) `1 } ) assume A6: x in (v_strip (G,i)) /\ (v_strip (G,(i + 1))) ; ::_thesis: x in { q where q is Point of (TOP-REAL 2) : q `1 = (G * ((i + 1),1)) `1 } then A7: x in v_strip (G,i) by XBOOLE_0:def_4; A8: x in v_strip (G,(i + 1)) by A6, XBOOLE_0:def_4; reconsider p = x as Point of (TOP-REAL 2) by A6; percases ( ( i = 0 & i + 1 = len G ) or ( i = 0 & i + 1 <> len G ) or ( i <> 0 & i + 1 = len G ) or ( i <> 0 & i + 1 <> len G ) ) ; supposethat A9: i = 0 and A10: i + 1 = len G ; ::_thesis: x in { q where q is Point of (TOP-REAL 2) : q `1 = (G * ((i + 1),1)) `1 } v_strip (G,i) = { |[r,s]| where r, s is Real : r <= (G * ((0 + 1),1)) `1 } by A1, A4, A9, Th10; then consider r1, s1 being Real such that A11: x = |[r1,s1]| and A12: r1 <= (G * (1,1)) `1 by A7; v_strip (G,(len G)) = { |[r,s]| where r, s is Real : (G * ((len G),1)) `1 <= r } by A1, A4, Th9; then consider r2, s2 being Real such that A13: x = |[r2,s2]| and A14: (G * ((i + 1),1)) `1 <= r2 by A8, A10; r1 = |[r2,s2]| `1 by A11, A13, EUCLID:52 .= r2 by EUCLID:52 ; then (G * ((i + 1),1)) `1 = r1 by A9, A12, A14, XXREAL_0:1; then (G * ((i + 1),1)) `1 = p `1 by A11, EUCLID:52; hence x in { q where q is Point of (TOP-REAL 2) : q `1 = (G * ((i + 1),1)) `1 } ; ::_thesis: verum end; supposethat A15: i = 0 and A16: i + 1 <> len G ; ::_thesis: x in { q where q is Point of (TOP-REAL 2) : q `1 = (G * ((i + 1),1)) `1 } v_strip (G,i) = { |[r,s]| where r, s is Real : r <= (G * ((0 + 1),1)) `1 } by A1, A4, A15, Th10; then consider r1, s1 being Real such that A17: x = |[r1,s1]| and A18: r1 <= (G * (1,1)) `1 by A7; i + 1 < len G by A3, A16, XXREAL_0:1; then v_strip (G,(i + 1)) = { |[r,s]| where r, s is Real : ( (G * ((0 + 1),1)) `1 <= r & r <= (G * (((0 + 1) + 1),1)) `1 ) } by A1, A4, A15, Th8; then consider r2, s2 being Real such that A19: x = |[r2,s2]| and A20: (G * (1,1)) `1 <= r2 and r2 <= (G * ((1 + 1),1)) `1 by A8; r1 = |[r2,s2]| `1 by A17, A19, EUCLID:52 .= r2 by EUCLID:52 ; then (G * (1,1)) `1 = r1 by A18, A20, XXREAL_0:1; then (G * (1,1)) `1 = p `1 by A17, EUCLID:52; hence x in { q where q is Point of (TOP-REAL 2) : q `1 = (G * ((i + 1),1)) `1 } by A15; ::_thesis: verum end; supposethat A21: i <> 0 and A22: i + 1 = len G ; ::_thesis: x in { q where q is Point of (TOP-REAL 2) : q `1 = (G * ((i + 1),1)) `1 } A23: 1 <= i by A21, NAT_1:14; i < len G by A3, NAT_1:13; then v_strip (G,i) = { |[r,s]| where r, s is Real : ( (G * (i,1)) `1 <= r & r <= (G * ((i + 1),1)) `1 ) } by A1, A4, A23, Th8; then consider r1, s1 being Real such that A24: x = |[r1,s1]| and (G * (i,1)) `1 <= r1 and A25: r1 <= (G * ((i + 1),1)) `1 by A7; v_strip (G,(len G)) = { |[r,s]| where r, s is Real : (G * ((len G),1)) `1 <= r } by A1, A4, Th9; then consider r2, s2 being Real such that A26: x = |[r2,s2]| and A27: (G * ((i + 1),1)) `1 <= r2 by A8, A22; r1 = |[r2,s2]| `1 by A24, A26, EUCLID:52 .= r2 by EUCLID:52 ; then (G * ((i + 1),1)) `1 = r1 by A25, A27, XXREAL_0:1; then (G * ((i + 1),1)) `1 = p `1 by A24, EUCLID:52; hence x in { q where q is Point of (TOP-REAL 2) : q `1 = (G * ((i + 1),1)) `1 } ; ::_thesis: verum end; supposethat A28: i <> 0 and A29: i + 1 <> len G ; ::_thesis: x in { q where q is Point of (TOP-REAL 2) : q `1 = (G * ((i + 1),1)) `1 } A30: 1 <= i by A28, NAT_1:14; i < len G by A3, NAT_1:13; then v_strip (G,i) = { |[r,s]| where r, s is Real : ( (G * (i,1)) `1 <= r & r <= (G * ((i + 1),1)) `1 ) } by A1, A4, A30, Th8; then consider r1, s1 being Real such that A31: x = |[r1,s1]| and (G * (i,1)) `1 <= r1 and A32: r1 <= (G * ((i + 1),1)) `1 by A7; A33: 1 <= i + 1 by NAT_1:11; i + 1 < len G by A3, A29, XXREAL_0:1; then v_strip (G,(i + 1)) = { |[r,s]| where r, s is Real : ( (G * ((i + 1),1)) `1 <= r & r <= (G * (((i + 1) + 1),1)) `1 ) } by A1, A4, A33, Th8; then consider r2, s2 being Real such that A34: x = |[r2,s2]| and A35: (G * ((i + 1),1)) `1 <= r2 and r2 <= (G * (((i + 1) + 1),1)) `1 by A8; r1 = |[r2,s2]| `1 by A31, A34, EUCLID:52 .= r2 by EUCLID:52 ; then (G * ((i + 1),1)) `1 = r1 by A32, A35, XXREAL_0:1; then (G * ((i + 1),1)) `1 = p `1 by A31, EUCLID:52; hence x in { q where q is Point of (TOP-REAL 2) : q `1 = (G * ((i + 1),1)) `1 } ; ::_thesis: verum end; end; end; A36: { q where q is Point of (TOP-REAL 2) : q `1 = (G * ((i + 1),1)) `1 } c= v_strip (G,i) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { q where q is Point of (TOP-REAL 2) : q `1 = (G * ((i + 1),1)) `1 } or x in v_strip (G,i) ) assume x in { q where q is Point of (TOP-REAL 2) : q `1 = (G * ((i + 1),1)) `1 } ; ::_thesis: x in v_strip (G,i) then consider p being Point of (TOP-REAL 2) such that A37: p = x and A38: p `1 = (G * ((i + 1),1)) `1 ; A39: p = |[(p `1),(p `2)]| by EUCLID:53; percases ( i = 0 or i >= 1 ) by NAT_1:14; supposeA40: i = 0 ; ::_thesis: x in v_strip (G,i) then v_strip (G,i) = { |[r,s]| where r, s is Real : r <= (G * (1,1)) `1 } by A1, A4, Th10; hence x in v_strip (G,i) by A37, A38, A39, A40; ::_thesis: verum end; supposeA41: i >= 1 ; ::_thesis: x in v_strip (G,i) then A42: v_strip (G,i) = { |[r,s]| where r, s is Real : ( (G * (i,1)) `1 <= r & r <= (G * ((i + 1),1)) `1 ) } by A1, A4, A5, Th8; i < i + 1 by XREAL_1:29; then (G * (i,1)) `1 < p `1 by A2, A3, A4, A38, A41, Th3; hence x in v_strip (G,i) by A37, A38, A39, A42; ::_thesis: verum end; end; end; { q where q is Point of (TOP-REAL 2) : q `1 = (G * ((i + 1),1)) `1 } c= v_strip (G,(i + 1)) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { q where q is Point of (TOP-REAL 2) : q `1 = (G * ((i + 1),1)) `1 } or x in v_strip (G,(i + 1)) ) assume x in { q where q is Point of (TOP-REAL 2) : q `1 = (G * ((i + 1),1)) `1 } ; ::_thesis: x in v_strip (G,(i + 1)) then consider p being Point of (TOP-REAL 2) such that A43: p = x and A44: p `1 = (G * ((i + 1),1)) `1 ; A45: p = |[(p `1),(p `2)]| by EUCLID:53; A46: 1 <= i + 1 by NAT_1:11; percases ( i + 1 = len G or i + 1 < len G ) by A3, XXREAL_0:1; supposeA47: i + 1 = len G ; ::_thesis: x in v_strip (G,(i + 1)) then v_strip (G,(i + 1)) = { |[r,s]| where r, s is Real : (G * ((len G),1)) `1 <= r } by A1, A4, Th9; hence x in v_strip (G,(i + 1)) by A43, A44, A45, A47; ::_thesis: verum end; supposeA48: i + 1 < len G ; ::_thesis: x in v_strip (G,(i + 1)) then A49: v_strip (G,(i + 1)) = { |[r,s]| where r, s is Real : ( (G * ((i + 1),1)) `1 <= r & r <= (G * (((i + 1) + 1),1)) `1 ) } by A1, A4, A46, Th8; A50: i + 1 < (i + 1) + 1 by NAT_1:13; (i + 1) + 1 <= len G by A48, NAT_1:13; then p `1 < (G * (((i + 1) + 1),1)) `1 by A2, A4, A44, A46, A50, Th3; hence x in v_strip (G,(i + 1)) by A43, A44, A45, A49; ::_thesis: verum end; end; end; hence { q where q is Point of (TOP-REAL 2) : q `1 = (G * ((i + 1),1)) `1 } c= (v_strip (G,i)) /\ (v_strip (G,(i + 1))) by A36, XBOOLE_1:19; ::_thesis: verum end; theorem Th24: :: GOBOARD5:24 for j being Element of NAT for G being Matrix of (TOP-REAL 2) st G is V3() & G is Y_equal-in-column & G is Y_increasing-in-line & j + 1 <= width G holds (h_strip (G,j)) /\ (h_strip (G,(j + 1))) = { q where q is Point of (TOP-REAL 2) : q `2 = (G * (1,(j + 1))) `2 } proof let j be Element of NAT ; ::_thesis: for G being Matrix of (TOP-REAL 2) st G is V3() & G is Y_equal-in-column & G is Y_increasing-in-line & j + 1 <= width G holds (h_strip (G,j)) /\ (h_strip (G,(j + 1))) = { q where q is Point of (TOP-REAL 2) : q `2 = (G * (1,(j + 1))) `2 } let G be Matrix of (TOP-REAL 2); ::_thesis: ( G is V3() & G is Y_equal-in-column & G is Y_increasing-in-line & j + 1 <= width G implies (h_strip (G,j)) /\ (h_strip (G,(j + 1))) = { q where q is Point of (TOP-REAL 2) : q `2 = (G * (1,(j + 1))) `2 } ) assume that A1: ( G is V3() & G is Y_equal-in-column ) and A2: G is Y_increasing-in-line and A3: j + 1 <= width G ; ::_thesis: (h_strip (G,j)) /\ (h_strip (G,(j + 1))) = { q where q is Point of (TOP-REAL 2) : q `2 = (G * (1,(j + 1))) `2 } len G <> 0 by A1, GOBOARD1:def_3; then A4: 1 <= len G by NAT_1:14; A5: j < width G by A3, NAT_1:13; thus (h_strip (G,j)) /\ (h_strip (G,(j + 1))) c= { q where q is Point of (TOP-REAL 2) : q `2 = (G * (1,(j + 1))) `2 } :: according to XBOOLE_0:def_10 ::_thesis: { q where q is Point of (TOP-REAL 2) : q `2 = (G * (1,(j + 1))) `2 } c= (h_strip (G,j)) /\ (h_strip (G,(j + 1))) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (h_strip (G,j)) /\ (h_strip (G,(j + 1))) or x in { q where q is Point of (TOP-REAL 2) : q `2 = (G * (1,(j + 1))) `2 } ) assume A6: x in (h_strip (G,j)) /\ (h_strip (G,(j + 1))) ; ::_thesis: x in { q where q is Point of (TOP-REAL 2) : q `2 = (G * (1,(j + 1))) `2 } then A7: x in h_strip (G,j) by XBOOLE_0:def_4; A8: x in h_strip (G,(j + 1)) by A6, XBOOLE_0:def_4; reconsider p = x as Point of (TOP-REAL 2) by A6; percases ( ( j = 0 & j + 1 = width G ) or ( j = 0 & j + 1 <> width G ) or ( j <> 0 & j + 1 = width G ) or ( j <> 0 & j + 1 <> width G ) ) ; supposethat A9: j = 0 and A10: j + 1 = width G ; ::_thesis: x in { q where q is Point of (TOP-REAL 2) : q `2 = (G * (1,(j + 1))) `2 } h_strip (G,j) = { |[r,s]| where r, s is Real : s <= (G * (1,(0 + 1))) `2 } by A1, A4, A9, Th7; then consider r1, s1 being Real such that A11: x = |[r1,s1]| and A12: s1 <= (G * (1,1)) `2 by A7; h_strip (G,(width G)) = { |[r,s]| where r, s is Real : (G * (1,(width G))) `2 <= s } by A1, A4, Th6; then consider r2, s2 being Real such that A13: x = |[r2,s2]| and A14: (G * (1,(j + 1))) `2 <= s2 by A8, A10; s1 = |[r2,s2]| `2 by A11, A13, EUCLID:52 .= s2 by EUCLID:52 ; then (G * (1,(j + 1))) `2 = s1 by A9, A12, A14, XXREAL_0:1; then (G * (1,(j + 1))) `2 = p `2 by A11, EUCLID:52; hence x in { q where q is Point of (TOP-REAL 2) : q `2 = (G * (1,(j + 1))) `2 } ; ::_thesis: verum end; supposethat A15: j = 0 and A16: j + 1 <> width G ; ::_thesis: x in { q where q is Point of (TOP-REAL 2) : q `2 = (G * (1,(j + 1))) `2 } h_strip (G,j) = { |[r,s]| where r, s is Real : s <= (G * (1,(0 + 1))) `2 } by A1, A4, A15, Th7; then consider r1, s1 being Real such that A17: x = |[r1,s1]| and A18: s1 <= (G * (1,1)) `2 by A7; j + 1 < width G by A3, A16, XXREAL_0:1; then h_strip (G,(j + 1)) = { |[r,s]| where r, s is Real : ( (G * (1,(0 + 1))) `2 <= s & s <= (G * (1,((0 + 1) + 1))) `2 ) } by A1, A4, A15, Th5; then consider r2, s2 being Real such that A19: x = |[r2,s2]| and A20: (G * (1,1)) `2 <= s2 and s2 <= (G * (1,(1 + 1))) `2 by A8; s1 = |[r2,s2]| `2 by A17, A19, EUCLID:52 .= s2 by EUCLID:52 ; then (G * (1,1)) `2 = s1 by A18, A20, XXREAL_0:1; then (G * (1,1)) `2 = p `2 by A17, EUCLID:52; hence x in { q where q is Point of (TOP-REAL 2) : q `2 = (G * (1,(j + 1))) `2 } by A15; ::_thesis: verum end; supposethat A21: j <> 0 and A22: j + 1 = width G ; ::_thesis: x in { q where q is Point of (TOP-REAL 2) : q `2 = (G * (1,(j + 1))) `2 } A23: 1 <= j by A21, NAT_1:14; j < width G by A3, NAT_1:13; then h_strip (G,j) = { |[r,s]| where r, s is Real : ( (G * (1,j)) `2 <= s & s <= (G * (1,(j + 1))) `2 ) } by A1, A4, A23, Th5; then consider r1, s1 being Real such that A24: x = |[r1,s1]| and (G * (1,j)) `2 <= s1 and A25: s1 <= (G * (1,(j + 1))) `2 by A7; h_strip (G,(width G)) = { |[r,s]| where r, s is Real : (G * (1,(width G))) `2 <= s } by A1, A4, Th6; then consider r2, s2 being Real such that A26: x = |[r2,s2]| and A27: (G * (1,(j + 1))) `2 <= s2 by A8, A22; s1 = |[r2,s2]| `2 by A24, A26, EUCLID:52 .= s2 by EUCLID:52 ; then (G * (1,(j + 1))) `2 = s1 by A25, A27, XXREAL_0:1; then (G * (1,(j + 1))) `2 = p `2 by A24, EUCLID:52; hence x in { q where q is Point of (TOP-REAL 2) : q `2 = (G * (1,(j + 1))) `2 } ; ::_thesis: verum end; supposethat A28: j <> 0 and A29: j + 1 <> width G ; ::_thesis: x in { q where q is Point of (TOP-REAL 2) : q `2 = (G * (1,(j + 1))) `2 } A30: 1 <= j by A28, NAT_1:14; j < width G by A3, NAT_1:13; then h_strip (G,j) = { |[r,s]| where r, s is Real : ( (G * (1,j)) `2 <= s & s <= (G * (1,(j + 1))) `2 ) } by A1, A4, A30, Th5; then consider r1, s1 being Real such that A31: x = |[r1,s1]| and (G * (1,j)) `2 <= s1 and A32: s1 <= (G * (1,(j + 1))) `2 by A7; A33: 1 <= j + 1 by NAT_1:11; j + 1 < width G by A3, A29, XXREAL_0:1; then h_strip (G,(j + 1)) = { |[r,s]| where r, s is Real : ( (G * (1,(j + 1))) `2 <= s & s <= (G * (1,((j + 1) + 1))) `2 ) } by A1, A4, A33, Th5; then consider r2, s2 being Real such that A34: x = |[r2,s2]| and A35: (G * (1,(j + 1))) `2 <= s2 and s2 <= (G * (1,((j + 1) + 1))) `2 by A8; s1 = |[r2,s2]| `2 by A31, A34, EUCLID:52 .= s2 by EUCLID:52 ; then (G * (1,(j + 1))) `2 = s1 by A32, A35, XXREAL_0:1; then (G * (1,(j + 1))) `2 = p `2 by A31, EUCLID:52; hence x in { q where q is Point of (TOP-REAL 2) : q `2 = (G * (1,(j + 1))) `2 } ; ::_thesis: verum end; end; end; A36: { q where q is Point of (TOP-REAL 2) : q `2 = (G * (1,(j + 1))) `2 } c= h_strip (G,j) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { q where q is Point of (TOP-REAL 2) : q `2 = (G * (1,(j + 1))) `2 } or x in h_strip (G,j) ) assume x in { q where q is Point of (TOP-REAL 2) : q `2 = (G * (1,(j + 1))) `2 } ; ::_thesis: x in h_strip (G,j) then consider p being Point of (TOP-REAL 2) such that A37: p = x and A38: p `2 = (G * (1,(j + 1))) `2 ; A39: p = |[(p `1),(p `2)]| by EUCLID:53; percases ( j = 0 or j >= 1 ) by NAT_1:14; supposeA40: j = 0 ; ::_thesis: x in h_strip (G,j) then h_strip (G,j) = { |[r,s]| where r, s is Real : s <= (G * (1,1)) `2 } by A1, A4, Th7; hence x in h_strip (G,j) by A37, A38, A39, A40; ::_thesis: verum end; supposeA41: j >= 1 ; ::_thesis: x in h_strip (G,j) then A42: h_strip (G,j) = { |[r,s]| where r, s is Real : ( (G * (1,j)) `2 <= s & s <= (G * (1,(j + 1))) `2 ) } by A1, A4, A5, Th5; j < j + 1 by XREAL_1:29; then (G * (1,j)) `2 < p `2 by A2, A3, A4, A38, A41, Th4; hence x in h_strip (G,j) by A37, A38, A39, A42; ::_thesis: verum end; end; end; { q where q is Point of (TOP-REAL 2) : q `2 = (G * (1,(j + 1))) `2 } c= h_strip (G,(j + 1)) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { q where q is Point of (TOP-REAL 2) : q `2 = (G * (1,(j + 1))) `2 } or x in h_strip (G,(j + 1)) ) assume x in { q where q is Point of (TOP-REAL 2) : q `2 = (G * (1,(j + 1))) `2 } ; ::_thesis: x in h_strip (G,(j + 1)) then consider p being Point of (TOP-REAL 2) such that A43: p = x and A44: p `2 = (G * (1,(j + 1))) `2 ; A45: p = |[(p `1),(p `2)]| by EUCLID:53; A46: 1 <= j + 1 by NAT_1:11; percases ( j + 1 = width G or j + 1 < width G ) by A3, XXREAL_0:1; supposeA47: j + 1 = width G ; ::_thesis: x in h_strip (G,(j + 1)) then h_strip (G,(j + 1)) = { |[r,s]| where r, s is Real : (G * (1,(width G))) `2 <= s } by A1, A4, Th6; hence x in h_strip (G,(j + 1)) by A43, A44, A45, A47; ::_thesis: verum end; supposeA48: j + 1 < width G ; ::_thesis: x in h_strip (G,(j + 1)) then A49: h_strip (G,(j + 1)) = { |[r,s]| where r, s is Real : ( (G * (1,(j + 1))) `2 <= s & s <= (G * (1,((j + 1) + 1))) `2 ) } by A1, A4, A46, Th5; A50: j + 1 < (j + 1) + 1 by NAT_1:13; (j + 1) + 1 <= width G by A48, NAT_1:13; then p `2 < (G * (1,((j + 1) + 1))) `2 by A2, A4, A44, A46, A50, Th4; hence x in h_strip (G,(j + 1)) by A43, A44, A45, A49; ::_thesis: verum end; end; end; hence { q where q is Point of (TOP-REAL 2) : q `2 = (G * (1,(j + 1))) `2 } c= (h_strip (G,j)) /\ (h_strip (G,(j + 1))) by A36, XBOOLE_1:19; ::_thesis: verum end; theorem Th25: :: GOBOARD5:25 for i, j being Element of NAT for G being Go-board st i < len G & 1 <= j & j < width G holds (cell (G,i,j)) /\ (cell (G,(i + 1),j)) = LSeg ((G * ((i + 1),j)),(G * ((i + 1),(j + 1)))) proof let i, j be Element of NAT ; ::_thesis: for G being Go-board st i < len G & 1 <= j & j < width G holds (cell (G,i,j)) /\ (cell (G,(i + 1),j)) = LSeg ((G * ((i + 1),j)),(G * ((i + 1),(j + 1)))) let G be Go-board; ::_thesis: ( i < len G & 1 <= j & j < width G implies (cell (G,i,j)) /\ (cell (G,(i + 1),j)) = LSeg ((G * ((i + 1),j)),(G * ((i + 1),(j + 1)))) ) assume that A1: i < len G and A2: 1 <= j and A3: j < width G ; ::_thesis: (cell (G,i,j)) /\ (cell (G,(i + 1),j)) = LSeg ((G * ((i + 1),j)),(G * ((i + 1),(j + 1)))) 0 <= i by NAT_1:2; then A4: 0 + 1 <= i + 1 by XREAL_1:6; A5: i + 1 <= len G by A1, NAT_1:13; thus (cell (G,i,j)) /\ (cell (G,(i + 1),j)) c= LSeg ((G * ((i + 1),j)),(G * ((i + 1),(j + 1)))) :: according to XBOOLE_0:def_10 ::_thesis: LSeg ((G * ((i + 1),j)),(G * ((i + 1),(j + 1)))) c= (cell (G,i,j)) /\ (cell (G,(i + 1),j)) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (cell (G,i,j)) /\ (cell (G,(i + 1),j)) or x in LSeg ((G * ((i + 1),j)),(G * ((i + 1),(j + 1)))) ) A6: (cell (G,i,j)) /\ (cell (G,(i + 1),j)) = (v_strip (G,i)) /\ (((v_strip (G,(i + 1))) /\ (h_strip (G,j))) /\ (h_strip (G,j))) by XBOOLE_1:16 .= (v_strip (G,i)) /\ ((v_strip (G,(i + 1))) /\ ((h_strip (G,j)) /\ (h_strip (G,j)))) by XBOOLE_1:16 .= ((v_strip (G,i)) /\ (v_strip (G,(i + 1)))) /\ (h_strip (G,j)) by XBOOLE_1:16 ; assume A7: x in (cell (G,i,j)) /\ (cell (G,(i + 1),j)) ; ::_thesis: x in LSeg ((G * ((i + 1),j)),(G * ((i + 1),(j + 1)))) then A8: x in (v_strip (G,i)) /\ (v_strip (G,(i + 1))) by A6, XBOOLE_0:def_4; A9: x in h_strip (G,j) by A6, A7, XBOOLE_0:def_4; A10: j < j + 1 by NAT_1:13; A11: j + 1 <= width G by A3, NAT_1:13; then A12: (G * ((i + 1),j)) `2 < (G * ((i + 1),(j + 1))) `2 by A2, A4, A5, A10, Th4; A13: G * ((i + 1),j) = |[((G * ((i + 1),j)) `1),((G * ((i + 1),j)) `2)]| by EUCLID:53; A14: j + 1 >= 1 by NAT_1:11; (G * ((i + 1),j)) `1 = (G * ((i + 1),1)) `1 by A2, A3, A4, A5, Th2 .= (G * ((i + 1),(j + 1))) `1 by A4, A5, A11, A14, Th2 ; then A15: G * ((i + 1),(j + 1)) = |[((G * ((i + 1),j)) `1),((G * ((i + 1),(j + 1))) `2)]| by EUCLID:53; reconsider p = x as Point of (TOP-REAL 2) by A7; i + 1 <= len G by A1, NAT_1:13; then p in { q where q is Point of (TOP-REAL 2) : q `1 = (G * ((i + 1),1)) `1 } by A8, Th23; then ex q being Point of (TOP-REAL 2) st ( q = p & q `1 = (G * ((i + 1),1)) `1 ) ; then A16: p `1 = (G * ((i + 1),j)) `1 by A2, A3, A4, A5, Th2; p in { |[r,s]| where r, s is Real : ( (G * ((i + 1),j)) `2 <= s & s <= (G * ((i + 1),(j + 1))) `2 ) } by A2, A3, A4, A5, A9, Th5; then A17: ex r, s being Real st ( p = |[r,s]| & (G * ((i + 1),j)) `2 <= s & s <= (G * ((i + 1),(j + 1))) `2 ) ; then A18: (G * ((i + 1),j)) `2 <= p `2 by EUCLID:52; p `2 <= (G * ((i + 1),(j + 1))) `2 by A17, EUCLID:52; then p in { q where q is Point of (TOP-REAL 2) : ( q `1 = (G * ((i + 1),j)) `1 & (G * ((i + 1),j)) `2 <= q `2 & q `2 <= (G * ((i + 1),(j + 1))) `2 ) } by A16, A18; hence x in LSeg ((G * ((i + 1),j)),(G * ((i + 1),(j + 1)))) by A12, A13, A15, TOPREAL3:9; ::_thesis: verum end; A19: LSeg ((G * ((i + 1),j)),(G * ((i + 1),(j + 1)))) c= cell (G,i,j) by A1, A2, A3, Th18; LSeg ((G * ((i + 1),j)),(G * ((i + 1),(j + 1)))) c= cell (G,(i + 1),j) by A2, A3, A4, A5, Th19; hence LSeg ((G * ((i + 1),j)),(G * ((i + 1),(j + 1)))) c= (cell (G,i,j)) /\ (cell (G,(i + 1),j)) by A19, XBOOLE_1:19; ::_thesis: verum end; theorem Th26: :: GOBOARD5:26 for j, i being Element of NAT for G being Go-board st j < width G & 1 <= i & i < len G holds (cell (G,i,j)) /\ (cell (G,i,(j + 1))) = LSeg ((G * (i,(j + 1))),(G * ((i + 1),(j + 1)))) proof let j, i be Element of NAT ; ::_thesis: for G being Go-board st j < width G & 1 <= i & i < len G holds (cell (G,i,j)) /\ (cell (G,i,(j + 1))) = LSeg ((G * (i,(j + 1))),(G * ((i + 1),(j + 1)))) let G be Go-board; ::_thesis: ( j < width G & 1 <= i & i < len G implies (cell (G,i,j)) /\ (cell (G,i,(j + 1))) = LSeg ((G * (i,(j + 1))),(G * ((i + 1),(j + 1)))) ) assume that A1: j < width G and A2: 1 <= i and A3: i < len G ; ::_thesis: (cell (G,i,j)) /\ (cell (G,i,(j + 1))) = LSeg ((G * (i,(j + 1))),(G * ((i + 1),(j + 1)))) 0 <= j by NAT_1:2; then A4: 0 + 1 <= j + 1 by XREAL_1:6; A5: j + 1 <= width G by A1, NAT_1:13; thus (cell (G,i,j)) /\ (cell (G,i,(j + 1))) c= LSeg ((G * (i,(j + 1))),(G * ((i + 1),(j + 1)))) :: according to XBOOLE_0:def_10 ::_thesis: LSeg ((G * (i,(j + 1))),(G * ((i + 1),(j + 1)))) c= (cell (G,i,j)) /\ (cell (G,i,(j + 1))) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (cell (G,i,j)) /\ (cell (G,i,(j + 1))) or x in LSeg ((G * (i,(j + 1))),(G * ((i + 1),(j + 1)))) ) A6: (cell (G,i,j)) /\ (cell (G,i,(j + 1))) = (h_strip (G,j)) /\ (((h_strip (G,(j + 1))) /\ (v_strip (G,i))) /\ (v_strip (G,i))) by XBOOLE_1:16 .= (h_strip (G,j)) /\ ((h_strip (G,(j + 1))) /\ ((v_strip (G,i)) /\ (v_strip (G,i)))) by XBOOLE_1:16 .= ((h_strip (G,j)) /\ (h_strip (G,(j + 1)))) /\ (v_strip (G,i)) by XBOOLE_1:16 ; assume A7: x in (cell (G,i,j)) /\ (cell (G,i,(j + 1))) ; ::_thesis: x in LSeg ((G * (i,(j + 1))),(G * ((i + 1),(j + 1)))) then A8: x in (h_strip (G,j)) /\ (h_strip (G,(j + 1))) by A6, XBOOLE_0:def_4; A9: x in v_strip (G,i) by A6, A7, XBOOLE_0:def_4; A10: i < i + 1 by NAT_1:13; A11: i + 1 <= len G by A3, NAT_1:13; then A12: (G * (i,(j + 1))) `1 < (G * ((i + 1),(j + 1))) `1 by A2, A4, A5, A10, Th3; A13: G * (i,(j + 1)) = |[((G * (i,(j + 1))) `1),((G * (i,(j + 1))) `2)]| by EUCLID:53; A14: i + 1 >= 1 by NAT_1:11; (G * (i,(j + 1))) `2 = (G * (1,(j + 1))) `2 by A2, A3, A4, A5, Th1 .= (G * ((i + 1),(j + 1))) `2 by A4, A5, A11, A14, Th1 ; then A15: G * ((i + 1),(j + 1)) = |[((G * ((i + 1),(j + 1))) `1),((G * (i,(j + 1))) `2)]| by EUCLID:53; reconsider p = x as Point of (TOP-REAL 2) by A7; j + 1 <= width G by A1, NAT_1:13; then p in { q where q is Point of (TOP-REAL 2) : q `2 = (G * (1,(j + 1))) `2 } by A8, Th24; then ex q being Point of (TOP-REAL 2) st ( q = p & q `2 = (G * (1,(j + 1))) `2 ) ; then A16: p `2 = (G * (i,(j + 1))) `2 by A2, A3, A4, A5, Th1; p in { |[r,s]| where r, s is Real : ( (G * (i,(j + 1))) `1 <= r & r <= (G * ((i + 1),(j + 1))) `1 ) } by A2, A3, A4, A5, A9, Th8; then A17: ex r, s being Real st ( p = |[r,s]| & (G * (i,(j + 1))) `1 <= r & r <= (G * ((i + 1),(j + 1))) `1 ) ; then A18: (G * (i,(j + 1))) `1 <= p `1 by EUCLID:52; p `1 <= (G * ((i + 1),(j + 1))) `1 by A17, EUCLID:52; then p in { q where q is Point of (TOP-REAL 2) : ( q `2 = (G * (i,(j + 1))) `2 & (G * (i,(j + 1))) `1 <= q `1 & q `1 <= (G * ((i + 1),(j + 1))) `1 ) } by A16, A18; hence x in LSeg ((G * (i,(j + 1))),(G * ((i + 1),(j + 1)))) by A12, A13, A15, TOPREAL3:10; ::_thesis: verum end; A19: LSeg ((G * (i,(j + 1))),(G * ((i + 1),(j + 1)))) c= cell (G,i,j) by A1, A2, A3, Th21; LSeg ((G * (i,(j + 1))),(G * ((i + 1),(j + 1)))) c= cell (G,i,(j + 1)) by A2, A3, A4, A5, Th22; hence LSeg ((G * (i,(j + 1))),(G * ((i + 1),(j + 1)))) c= (cell (G,i,j)) /\ (cell (G,i,(j + 1))) by A19, XBOOLE_1:19; ::_thesis: verum end; theorem Th27: :: GOBOARD5:27 for k, i, j being Element of NAT for f being standard special_circular_sequence st 1 <= k & k + 1 <= len f & [(i + 1),j] in Indices (GoB f) & [(i + 1),(j + 1)] in Indices (GoB f) & f /. k = (GoB f) * ((i + 1),j) & f /. (k + 1) = (GoB f) * ((i + 1),(j + 1)) holds ( left_cell (f,k) = cell ((GoB f),i,j) & right_cell (f,k) = cell ((GoB f),(i + 1),j) ) proof let k, i, j be Element of NAT ; ::_thesis: for f being standard special_circular_sequence st 1 <= k & k + 1 <= len f & [(i + 1),j] in Indices (GoB f) & [(i + 1),(j + 1)] in Indices (GoB f) & f /. k = (GoB f) * ((i + 1),j) & f /. (k + 1) = (GoB f) * ((i + 1),(j + 1)) holds ( left_cell (f,k) = cell ((GoB f),i,j) & right_cell (f,k) = cell ((GoB f),(i + 1),j) ) let f be standard special_circular_sequence; ::_thesis: ( 1 <= k & k + 1 <= len f & [(i + 1),j] in Indices (GoB f) & [(i + 1),(j + 1)] in Indices (GoB f) & f /. k = (GoB f) * ((i + 1),j) & f /. (k + 1) = (GoB f) * ((i + 1),(j + 1)) implies ( left_cell (f,k) = cell ((GoB f),i,j) & right_cell (f,k) = cell ((GoB f),(i + 1),j) ) ) assume that A1: 1 <= k and A2: k + 1 <= len f and A3: [(i + 1),j] in Indices (GoB f) and A4: [(i + 1),(j + 1)] in Indices (GoB f) and A5: f /. k = (GoB f) * ((i + 1),j) and A6: f /. (k + 1) = (GoB f) * ((i + 1),(j + 1)) ; ::_thesis: ( left_cell (f,k) = cell ((GoB f),i,j) & right_cell (f,k) = cell ((GoB f),(i + 1),j) ) A7: j < j + 1 by XREAL_1:29; A8: j + 1 <= (j + 1) + 1 by NAT_1:11; hence left_cell (f,k) = cell ((GoB f),((i + 1) -' 1),j) by A1, A2, A3, A4, A5, A6, A7, Def7 .= cell ((GoB f),i,j) by NAT_D:34 ; ::_thesis: right_cell (f,k) = cell ((GoB f),(i + 1),j) thus right_cell (f,k) = cell ((GoB f),(i + 1),j) by A1, A2, A3, A4, A5, A6, A7, A8, Def6; ::_thesis: verum end; theorem Th28: :: GOBOARD5:28 for k, i, j being Element of NAT for f being standard special_circular_sequence st 1 <= k & k + 1 <= len f & [i,(j + 1)] in Indices (GoB f) & [(i + 1),(j + 1)] in Indices (GoB f) & f /. k = (GoB f) * (i,(j + 1)) & f /. (k + 1) = (GoB f) * ((i + 1),(j + 1)) holds ( left_cell (f,k) = cell ((GoB f),i,(j + 1)) & right_cell (f,k) = cell ((GoB f),i,j) ) proof let k, i, j be Element of NAT ; ::_thesis: for f being standard special_circular_sequence st 1 <= k & k + 1 <= len f & [i,(j + 1)] in Indices (GoB f) & [(i + 1),(j + 1)] in Indices (GoB f) & f /. k = (GoB f) * (i,(j + 1)) & f /. (k + 1) = (GoB f) * ((i + 1),(j + 1)) holds ( left_cell (f,k) = cell ((GoB f),i,(j + 1)) & right_cell (f,k) = cell ((GoB f),i,j) ) let f be standard special_circular_sequence; ::_thesis: ( 1 <= k & k + 1 <= len f & [i,(j + 1)] in Indices (GoB f) & [(i + 1),(j + 1)] in Indices (GoB f) & f /. k = (GoB f) * (i,(j + 1)) & f /. (k + 1) = (GoB f) * ((i + 1),(j + 1)) implies ( left_cell (f,k) = cell ((GoB f),i,(j + 1)) & right_cell (f,k) = cell ((GoB f),i,j) ) ) assume that A1: 1 <= k and A2: k + 1 <= len f and A3: [i,(j + 1)] in Indices (GoB f) and A4: [(i + 1),(j + 1)] in Indices (GoB f) and A5: f /. k = (GoB f) * (i,(j + 1)) and A6: f /. (k + 1) = (GoB f) * ((i + 1),(j + 1)) ; ::_thesis: ( left_cell (f,k) = cell ((GoB f),i,(j + 1)) & right_cell (f,k) = cell ((GoB f),i,j) ) A7: i < i + 1 by XREAL_1:29; A8: i + 1 <= (i + 1) + 1 by NAT_1:11; hence left_cell (f,k) = cell ((GoB f),i,(j + 1)) by A1, A2, A3, A4, A5, A6, A7, Def7; ::_thesis: right_cell (f,k) = cell ((GoB f),i,j) thus right_cell (f,k) = cell ((GoB f),i,((j + 1) -' 1)) by A1, A2, A3, A4, A5, A6, A7, A8, Def6 .= cell ((GoB f),i,j) by NAT_D:34 ; ::_thesis: verum end; theorem Th29: :: GOBOARD5:29 for k, i, j being Element of NAT for f being standard special_circular_sequence st 1 <= k & k + 1 <= len f & [i,(j + 1)] in Indices (GoB f) & [(i + 1),(j + 1)] in Indices (GoB f) & f /. k = (GoB f) * ((i + 1),(j + 1)) & f /. (k + 1) = (GoB f) * (i,(j + 1)) holds ( left_cell (f,k) = cell ((GoB f),i,j) & right_cell (f,k) = cell ((GoB f),i,(j + 1)) ) proof let k, i, j be Element of NAT ; ::_thesis: for f being standard special_circular_sequence st 1 <= k & k + 1 <= len f & [i,(j + 1)] in Indices (GoB f) & [(i + 1),(j + 1)] in Indices (GoB f) & f /. k = (GoB f) * ((i + 1),(j + 1)) & f /. (k + 1) = (GoB f) * (i,(j + 1)) holds ( left_cell (f,k) = cell ((GoB f),i,j) & right_cell (f,k) = cell ((GoB f),i,(j + 1)) ) let f be standard special_circular_sequence; ::_thesis: ( 1 <= k & k + 1 <= len f & [i,(j + 1)] in Indices (GoB f) & [(i + 1),(j + 1)] in Indices (GoB f) & f /. k = (GoB f) * ((i + 1),(j + 1)) & f /. (k + 1) = (GoB f) * (i,(j + 1)) implies ( left_cell (f,k) = cell ((GoB f),i,j) & right_cell (f,k) = cell ((GoB f),i,(j + 1)) ) ) assume that A1: 1 <= k and A2: k + 1 <= len f and A3: [i,(j + 1)] in Indices (GoB f) and A4: [(i + 1),(j + 1)] in Indices (GoB f) and A5: f /. k = (GoB f) * ((i + 1),(j + 1)) and A6: f /. (k + 1) = (GoB f) * (i,(j + 1)) ; ::_thesis: ( left_cell (f,k) = cell ((GoB f),i,j) & right_cell (f,k) = cell ((GoB f),i,(j + 1)) ) A7: i < i + 1 by XREAL_1:29; A8: i + 1 <= (i + 1) + 1 by NAT_1:11; hence left_cell (f,k) = cell ((GoB f),i,((j + 1) -' 1)) by A1, A2, A3, A4, A5, A6, A7, Def7 .= cell ((GoB f),i,j) by NAT_D:34 ; ::_thesis: right_cell (f,k) = cell ((GoB f),i,(j + 1)) thus right_cell (f,k) = cell ((GoB f),i,(j + 1)) by A1, A2, A3, A4, A5, A6, A7, A8, Def6; ::_thesis: verum end; theorem Th30: :: GOBOARD5:30 for k, i, j being Element of NAT for f being standard special_circular_sequence st 1 <= k & k + 1 <= len f & [(i + 1),(j + 1)] in Indices (GoB f) & [(i + 1),j] in Indices (GoB f) & f /. k = (GoB f) * ((i + 1),(j + 1)) & f /. (k + 1) = (GoB f) * ((i + 1),j) holds ( left_cell (f,k) = cell ((GoB f),(i + 1),j) & right_cell (f,k) = cell ((GoB f),i,j) ) proof let k, i, j be Element of NAT ; ::_thesis: for f being standard special_circular_sequence st 1 <= k & k + 1 <= len f & [(i + 1),(j + 1)] in Indices (GoB f) & [(i + 1),j] in Indices (GoB f) & f /. k = (GoB f) * ((i + 1),(j + 1)) & f /. (k + 1) = (GoB f) * ((i + 1),j) holds ( left_cell (f,k) = cell ((GoB f),(i + 1),j) & right_cell (f,k) = cell ((GoB f),i,j) ) let f be standard special_circular_sequence; ::_thesis: ( 1 <= k & k + 1 <= len f & [(i + 1),(j + 1)] in Indices (GoB f) & [(i + 1),j] in Indices (GoB f) & f /. k = (GoB f) * ((i + 1),(j + 1)) & f /. (k + 1) = (GoB f) * ((i + 1),j) implies ( left_cell (f,k) = cell ((GoB f),(i + 1),j) & right_cell (f,k) = cell ((GoB f),i,j) ) ) assume that A1: 1 <= k and A2: k + 1 <= len f and A3: [(i + 1),(j + 1)] in Indices (GoB f) and A4: [(i + 1),j] in Indices (GoB f) and A5: f /. k = (GoB f) * ((i + 1),(j + 1)) and A6: f /. (k + 1) = (GoB f) * ((i + 1),j) ; ::_thesis: ( left_cell (f,k) = cell ((GoB f),(i + 1),j) & right_cell (f,k) = cell ((GoB f),i,j) ) A7: j < j + 1 by XREAL_1:29; A8: j + 1 <= (j + 1) + 1 by NAT_1:11; hence left_cell (f,k) = cell ((GoB f),(i + 1),j) by A1, A2, A3, A4, A5, A6, A7, Def7; ::_thesis: right_cell (f,k) = cell ((GoB f),i,j) thus right_cell (f,k) = cell ((GoB f),((i + 1) -' 1),j) by A1, A2, A3, A4, A5, A6, A7, A8, Def6 .= cell ((GoB f),i,j) by NAT_D:34 ; ::_thesis: verum end; theorem :: GOBOARD5:31 for k being Element of NAT for f being standard special_circular_sequence st 1 <= k & k + 1 <= len f holds (left_cell (f,k)) /\ (right_cell (f,k)) = LSeg (f,k) proof let k be Element of NAT ; ::_thesis: for f being standard special_circular_sequence st 1 <= k & k + 1 <= len f holds (left_cell (f,k)) /\ (right_cell (f,k)) = LSeg (f,k) let f be standard special_circular_sequence; ::_thesis: ( 1 <= k & k + 1 <= len f implies (left_cell (f,k)) /\ (right_cell (f,k)) = LSeg (f,k) ) assume that A1: 1 <= k and A2: k + 1 <= len f ; ::_thesis: (left_cell (f,k)) /\ (right_cell (f,k)) = LSeg (f,k) k <= k + 1 by NAT_1:11; then k <= len f by A2, XXREAL_0:2; then A3: k in dom f by A1, FINSEQ_3:25; then consider i1, j1 being Element of NAT such that A4: [i1,j1] in Indices (GoB f) and A5: f /. k = (GoB f) * (i1,j1) by Th11; k + 1 >= 1 by NAT_1:11; then A6: k + 1 in dom f by A2, FINSEQ_3:25; then consider i2, j2 being Element of NAT such that A7: [i2,j2] in Indices (GoB f) and A8: f /. (k + 1) = (GoB f) * (i2,j2) by Th11; A9: (abs (i1 - i2)) + (abs (j1 - j2)) = 1 by A3, A4, A5, A6, A7, A8, Th12; A10: now__::_thesis:_(_(_abs_(i1_-_i2)_=_1_&_j1_=_j2_&_(_i1_=_i2_+_1_or_i1_+_1_=_i2_)_&_j1_=_j2_)_or_(_i1_=_i2_&_abs_(j1_-_j2)_=_1_&_(_j1_=_j2_+_1_or_j1_+_1_=_j2_)_&_i1_=_i2_)_) percases ( ( abs (i1 - i2) = 1 & j1 = j2 ) or ( i1 = i2 & abs (j1 - j2) = 1 ) ) by A9, SEQM_3:42; casethat A11: abs (i1 - i2) = 1 and A12: j1 = j2 ; ::_thesis: ( ( i1 = i2 + 1 or i1 + 1 = i2 ) & j1 = j2 ) ( i1 - i2 = 1 or - (i1 - i2) = 1 ) by A11, ABSVALUE:def_1; hence ( i1 = i2 + 1 or i1 + 1 = i2 ) ; ::_thesis: j1 = j2 thus j1 = j2 by A12; ::_thesis: verum end; casethat A13: i1 = i2 and A14: abs (j1 - j2) = 1 ; ::_thesis: ( ( j1 = j2 + 1 or j1 + 1 = j2 ) & i1 = i2 ) ( j1 - j2 = 1 or - (j1 - j2) = 1 ) by A14, ABSVALUE:def_1; hence ( j1 = j2 + 1 or j1 + 1 = j2 ) ; ::_thesis: i1 = i2 thus i1 = i2 by A13; ::_thesis: verum end; end; end; A15: 0 + 1 <= j1 by A4, MATRIX_1:38; A16: j1 <= width (GoB f) by A4, MATRIX_1:38; A17: 1 <= j2 by A7, MATRIX_1:38; A18: j2 <= width (GoB f) by A7, MATRIX_1:38; A19: 0 + 1 <= i1 by A4, MATRIX_1:38; A20: i1 <= len (GoB f) by A4, MATRIX_1:38; A21: 1 <= i2 by A7, MATRIX_1:38; A22: i2 <= len (GoB f) by A7, MATRIX_1:38; i1 > 0 by A19, NAT_1:13; then consider i being Nat such that A23: i + 1 = i1 by NAT_1:6; reconsider i = i as Element of NAT by ORDINAL1:def_12; A24: i + 1 = i1 by A23; A25: i < len (GoB f) by A20, A23, NAT_1:13; j1 > 0 by A15, NAT_1:13; then consider j being Nat such that A26: j + 1 = j1 by NAT_1:6; reconsider j = j as Element of NAT by ORDINAL1:def_12; A27: j + 1 = j1 by A26; A28: j < width (GoB f) by A16, A26, NAT_1:13; percases ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A10; supposeA29: ( i1 = i2 & j1 + 1 = j2 ) ; ::_thesis: (left_cell (f,k)) /\ (right_cell (f,k)) = LSeg (f,k) then A30: j1 < width (GoB f) by A18, NAT_1:13; A31: left_cell (f,k) = cell ((GoB f),i,j1) by A1, A2, A4, A5, A7, A8, A23, A29, Th27; right_cell (f,k) = cell ((GoB f),i1,j1) by A1, A2, A4, A5, A7, A8, A24, A29, Th27; hence (left_cell (f,k)) /\ (right_cell (f,k)) = LSeg (((GoB f) * (i1,j1)),((GoB f) * (i1,(j1 + 1)))) by A15, A23, A25, A30, A31, Th25 .= LSeg (f,k) by A1, A2, A5, A8, A29, TOPREAL1:def_3 ; ::_thesis: verum end; supposeA32: ( i1 + 1 = i2 & j1 = j2 ) ; ::_thesis: (left_cell (f,k)) /\ (right_cell (f,k)) = LSeg (f,k) then A33: i1 < len (GoB f) by A22, NAT_1:13; A34: left_cell (f,k) = cell ((GoB f),i1,j1) by A1, A2, A4, A5, A7, A8, A27, A32, Th28; right_cell (f,k) = cell ((GoB f),i1,j) by A1, A2, A4, A5, A7, A8, A26, A32, Th28; hence (left_cell (f,k)) /\ (right_cell (f,k)) = LSeg (((GoB f) * (i1,j1)),((GoB f) * ((i1 + 1),j1))) by A19, A26, A28, A33, A34, Th26 .= LSeg (f,k) by A1, A2, A5, A8, A32, TOPREAL1:def_3 ; ::_thesis: verum end; supposeA35: ( i1 = i2 + 1 & j1 = j2 ) ; ::_thesis: (left_cell (f,k)) /\ (right_cell (f,k)) = LSeg (f,k) then A36: i2 < len (GoB f) by A20, NAT_1:13; A37: left_cell (f,k) = cell ((GoB f),i2,j) by A1, A2, A4, A5, A7, A8, A26, A35, Th29; right_cell (f,k) = cell ((GoB f),i2,j1) by A1, A2, A4, A5, A7, A8, A27, A35, Th29; hence (left_cell (f,k)) /\ (right_cell (f,k)) = LSeg (((GoB f) * ((i2 + 1),j1)),((GoB f) * (i2,j1))) by A21, A26, A28, A36, A37, Th26 .= LSeg (f,k) by A1, A2, A5, A8, A35, TOPREAL1:def_3 ; ::_thesis: verum end; supposeA38: ( i1 = i2 & j1 = j2 + 1 ) ; ::_thesis: (left_cell (f,k)) /\ (right_cell (f,k)) = LSeg (f,k) then A39: j2 < width (GoB f) by A16, NAT_1:13; A40: left_cell (f,k) = cell ((GoB f),i1,j2) by A1, A2, A4, A5, A7, A8, A24, A38, Th30; right_cell (f,k) = cell ((GoB f),i,j2) by A1, A2, A4, A5, A7, A8, A23, A38, Th30; hence (left_cell (f,k)) /\ (right_cell (f,k)) = LSeg (((GoB f) * (i1,(j2 + 1))),((GoB f) * (i1,j2))) by A17, A23, A25, A39, A40, Th25 .= LSeg (f,k) by A1, A2, A5, A8, A38, TOPREAL1:def_3 ; ::_thesis: verum end; end; end;